論理用語と型用語

Lean 論理 用語法
論理 型
命題 型
命題Pの証明 型Tの式
証明内の根拠 式内の定数名
含意 関数型
前件 域型〈ソース型〉
後件 余域型〈ターゲット型〉
シーケント プロファイル
仮定 コンテキスト
結論 ターゲット
証明 証拠式
定理記述 オブジェクト定義
公理記述 定数宣言
仮説記述 変数宣言