このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

Globular探り 3:定理の主セル

定理(theorem)は、公理や定義も含む。名前\stackrel{\sim}{=}式 の形に対応する。右辺にも名前が出現するが、その名前はセルの名前。右辺に出現する名前のなかでひとつだけが主セルの名前として特定されている。

「名前→式」の展開と「式→名前」の縮約がクリック操作で可能だが、縮約のときは、主セルをクリックする。その他のセルは反応しない。Theoremコマンドはいつでも使えるので、キャンバス内の図(diagram)はいつの時点でも主セルを持っているのだろう。

主セルを維持するための制限もあるはずだ。その制限のせいで自由な操作は出来なくなっているかも知れない。

Restrictコマンドがまだ分からない。

[追記]Restrictはたいした操作ではなかった。今、見えているダイアグラムをカレントのダイアグラムにして、元のダイアグラムを捨てる。ダイアグラムの一部を取り出して調べたい時には便利。[/追記]