R-En/Comp R-En/Proof computation proof let := have from lambda assume call use〈using〉 providing return suffices because where := try〈attemp〉 改行 return of showed from 同義語： obtain, show, clarify, describe, indicate, exhibit, prove,…

項と型の型付け〈typing〉チェック ＝ 証明と命題の演繹〈deduction〉チェック 型付けの宣言〈型宣言 | 型判断〉 ＝ 演繹の宣言〈命題判断〉 ＝ 無名定理 型付けの正しさ〈correctness〉＝ 演繹〈deduction〉の正しさ 項の型 ＝ 証明の結論命題〈ターゲット…

混合コンテキストは、次を混ぜたもの。 型宣言文 値割り当て文 型宣言文だけのコンテキスト（実体は依存レコード＝テレスコープ）は指標〈signature〉。型宣言されたすべての名前に値割り当てしたコンテキストは環境〈environment〉と呼ぶ。混合コンテキスト…