Globular探り 3:定理の主セル
定理(theorem)は、公理や定義も含む。名前式 の形に対応する。右辺にも名前が出現するが、その名前はセルの名前。右辺に出現する名前のなかでひとつだけが主セルの名前として特定されている。
「名前→式」の展開と「式→名前」の縮約がクリック操作で可能だが、縮約のときは、主セルをクリックする。その他のセルは反応しない。Theoremコマンドはいつでも使えるので、キャンバス内の図(diagram)はいつの時点でも主セルを持っているのだろう。
主セルを維持するための制限もあるはずだ。その制限のせいで自由な操作は出来なくなっているかも知れない。
Restrictコマンドがまだ分からない。
[追記]Restrictはたいした操作ではなかった。今、見えているダイアグラムをカレントのダイアグラムにして、元のダイアグラムを捨てる。ダイアグラムの一部を取り出して調べたい時には便利。[/追記]