| Type | Prop |
|---|---|
| プロファイル | シーケント |
| 型判断プロファイル | 命題判断シーケント |
| 型問題プロファイル | 命題問題シーケント |
| 計算合成〈synthesis〉 | 証明合成 |
| 計算合成コマンド | 証明合成コマンド |
| 順方向計算合成コマンド | 順方向証明合成コマンド |
| 逆方向計算合成コマンド | 逆方向証明合成コマンド |
| 計算譜(?) | 証明譜 |
| 計算構成問題 | 証明構成問題 |
| {計算}?項の{戻り値}?型推論 | 証明{項}?の結論{命題}?推論 |
| ライブラリ | {数学}?ライブラリ〈mathlib〉 |
- 計算合成コマンド＝計算コンビネータ＝コンビネータ
- 証明合成コマンド＝証明コンビネータ＝リーズニング
- 逆方向証明合成コマンド＝タクティク
- 計算譜＝計算スコア＝プログラム
- 証明譜＝証明スコア＝証明スクリプト≒タクティクスクリプト
- The Mathlib と a mathlib, mathlibs がある。
悪習と問題点：
- 判断〈主張〉と問題〈問い合わせ〉を区別しない。
- 順方向と逆方向を区別しない。
- プロファイル〈シーケント〉と射を区別しない。
- 命題と証明を区別しない（特に公理において）。
- 前提なし定理と前提あり定理を区別しない（演繹定理で合理化はできるが）。
- 型クラスインスタンス（増強手続き）と、一般的なモデルを区別しない。
- ライブラリに対するブラックボックス・ビューとホワイトボックス・ビューを区別しない／意識しない。
- ライブラリに対する知識ベース・ビューとツールボックス・ビューを区別しない／意識しない。
