ステージとコマンド

「状況」、「シーン」なども用語候補だが、「ステージ」を使う。コマンドは、ステージ上の判断／質問を操作する。またステージ自体もコマンドで操作する。

同じ名前に対して、フォワードコマンド doXxx とバックワードコマンド undoXxx がある。

全般的な管理コマンド：

1. New ステージ名 ： 現在のステージの子ステージを作る。ステージは入れ子にできる。
2. [α]> Remove i >[] ： ステージ上の項目（判断または質問）αを、その名前または番号 i を指定して削除する。
3. []> Put f >[α] ： ステージ上に項目 α を新規に置く。f は項目それ自体、項目のパック形式、ライブラリやコンテキスト内の名前または番号。
4. [Γ |-! A]> Enlarge >[Γ’ |-! A] ： 判断のコンテキストを増やす。
5. [Γ |-? A]> Shrink >[Γ’ |-? A] ： 質問のコンテキストを減らす。

フォワード・コマンド：

1. []> doObvious >[A |-! A] ： 明白な判断を無から生成する。
2. []> doWitness t >[Γ |-! A] ： 証拠 t を持つ判断を無から生成する。
3. [α]> doCurry >[α'] ： カリー化する。
4. [α]> doUncurry a >[α'] ： 反カリー化する。aは使用する名前。
5. [α1, ..., αn]> doPostComp f >[β] ： 関数 f を後結合する。
6. [αi]_{i∈)}> doTupple >[β] ： タプルを作る。
7. [αi]_{i∈)}> doCotupple >[β] ： コタプルを作る。

バックワード・コマンド：

1. [A |-? A]> undoObvious >[] ： 明白な質問を消す（無に帰す）。
2. [Γ |-? A]> undoWitness t >[] ： 証拠 t を持つ判断を消す（無に帰す）。
3. [α']> udoCurry a >[α] ： 反カリー化する。aは使用する名前。
4. [α']> undoUncurry >[α] ： カリー化する。
5. [β]> undoPostComp f >[α1, ..., αn] ： 関数 f を後結合する前の状態に戻す。
6. [β]> udoTupple >[αi]_{i∈)} ： タプルを分解する。
7. [β]> undoCotupple >[αi]_{i∈)} ： コタプルを分解する。