混合コンテキストが、次のレベルで提供される。
- ライブラリ
- パッケージ
- モジュール
- 名前空間
- セクション
- 関数・定理（のボディブロック）
- 入れ子ブロック（by, doなど）
これらの組織化機構〈organizing mechanism / feature〉は独立ではないし、一様でもない。構成される混合コンテキストは恣意的に区切られた〈fenced〉テレスコープになる。
コンテキスト／テレスコープの基本は名前の集合で、名前は：
- 宣言定数名： 代入〈割り当て〉ができない型付きの名前、axiom で導入。
- イミュータブル変数名： 代入〈割り当て〉が一度だけできる型付きの名前 variable で導入。引数リストでも導入される。
- 割り当て済み名前： イミュータブル変数名に割り当てを行ったもの。変更はできない。def, let, have で導入。
- ミュータブル変数名： 値の変更ができる名前、let mut で導入。
名前〈ラベル〉の型〈プロファイル〉宣言（命題宣言含む）と、型宣言済みの名前への項〈ボディ〉割り当てがテレスコープの中心。他に、定義的等式と項書き換え規則がコンテキストに入る。
関数のコンテキスト〈環境〉と引数、定理のコンテキストと前提の境界は曖昧で、どうとでも移動できる。構文的正規形として、コンテキストを最小化したパック形式〈カリー化形式〉と、コンテキストを最大化したアンパック形式〈アンカリー化形式〉がある。
名前達は、名前空間階層のなかに配置される。名前構造の操作に、open, export, namespace, section が使われる。Cリンケージとの名前のやり取りには、@[extern "名前"]、@[export 名前]。importはモジュールの操作だが、そのモジュールで定義された／取り込まれた名前の操作になる。
特定の機能性を持つ名前（関数名、定理名、型名／命題名）を探すのは困難。この困難が大きな障害になっている。
次は名付けの例：
namespace MyArith def one_plus_one_equals_two : Prop := 1 + 1 = 2 def one_plus_one_equals_three : Prop := 1 + 1 = 3 def x_plus_y_equals_ten (x y :Nat) : Prop := x + y = 10 end MyArith #check MyArith.one_plus_one_equals_two #check MyArith.x_plus_y_equals_ten
関数や定理は、名前で呼び出して使う。呼び出し時に、実引数を渡すかも知れない。関数を呼び出せば、戻り値と戻り型〈return type〉が得られる。得られた戻り値は名前に束縛されるかも知れない〈let, have〉。
宣言定数〈公理〉や関数〈定理〉から作られる項とは別に、コマンドとコマンドスクリプトがある。証明生成コマンドには、FRコマンド〈forward reasoning command〉とBRコマンド〈backward reasoning command〉がある。BRコマンドをタクティクとも呼ぶ。
リーズニングコマンドが相手にするのは、判断と質問〈問題 | ゴール〉が混じった証明状態〈proof state〉。コマンドは証明状態を遷移させる。証明状態の時間的遷移を空間的に描いた図をリーズニング図と呼ぶ。シーケント計算の証明図はリーズニング図である。
リーズニング図は、項を図示したストリング図や横棒図とは別物。しばしば混同される、無理もないが。
証明状態を遷移させるプログラムをリーズニング・コマンドスクリプトと言う。特にBRコマンド＝タクティクから作ったスクリプトはタクティク・スクリプト。
判断と質問が混じった証明状態を混合証明状態という。混合証明状態の遷移を記述した図を混合リーズニング図という。混合リーズニング図はツリーとは限らない。
リーズニング図は180度回転する反転〈inversion | conversse〉がある。反転は双対性と関係がある。
項の図示とリーズニングの図示は混同される。その理由のひとつは、項の図はリーズニング図に変換して埋め込めるから。項のスクリプトのノードは、post-composition, pre-composition としてリーズニングコマンドになり、図のリーズニングノードになる。
