証明項の帰結という言葉を入れてみる。 型理論 論理 計算項 証明項 計算項の型 証明項の帰結 型付け〈typing〉 帰結付け〈consequencing〉 型{付け}?判断 帰結{付け}?判断 型チェック 命題チェック? 帰結チェック? 項の検証? 証明{項}?の検証 項の型推論 証…

def Obj := Type def Enricher := Type def Hom (α β : Obj) : Enricher := (α → β) structure EndoFunctor where obj : Obj → Obj -- 台型構成子＝対象パート hom : {α β : Obj} → (Hom α β) → (Hom (obj α) (obj β)) -- ホムパート #check @EndoFunctor.ho…

mathlib と Std.logic も必要。 論理記号 導入規則 除去規則 連言∧ And.intro And.left, And.right 選言∨ Or.intro_left, Or.intro_right Or.elim 否定￢ Not.intro Not.elim〈absurd〉 真T True.intro 通常の証明 偽⊥ 背理法の証明 False.elim 含意→ ラムダ…

スキーマ、タプル空間、タプルインスタンス、フィールド関数、テーブル structure Schema where fields : Type typeAssig : fields → Type def TupleSpace (S : Schema) := ((f : S.fields) → S.typeAssig f) inductive NameAge where | name : NameAge | ag…