| Type | Prop |
|---|---|
| 型 | 命題 |
| 計算 | 証明 |
| 関数 | 定理 |
| 定数 | 前提なし定理 |
| 組み込み関数・定数 | 公理 |
| プロファイル | シーケント |
| フルかりー化プロファイル | 片側シーケント |
| 既存関数のプロファイル宣言 | 事実（定理の名前とシーケント） |
| サブルーチン（一例） | ルール |
| 型の要素 | 命題の証拠〈witness〉 |
| 型が非空 | 命題が証拠付き〈witnessed〉 |
| 引数変数〈仮の要素の名前〉 | 前提のラベル（仮の証拠の名前） |
| カリー同型 | 演繹定理 |
| カリー化 | 含意導入 |
| 関数の適用 | ルールの適用 |
| 関数・計算の結合 | ルール・証明のカット |
| {計算}?項の{戻り値}型 | 証明{項}?の結論{命題}? |
| {計算}?項のパラメータ変数 | 証明{項}?の前提ラベル |
プログラム＝計算アルゴリズム記述は実行されるが、証明＝証明アルゴリズム記述も実行される。前提の証拠が与えられると、それらを組み合わせて、結論の証拠を構成〈生成〉するのが、証明の実行。
タクティクによる証明はプログラム合成になっている。プログラム＝証明から新しいプログラムを作る。が、プロファイル＝シーケント＝ゴール をデータとして操作する。ゴールの意味は複ホムセットなので、個別の証明ではなくて証明一般を合成できる。
