def FooRetType (b:Bool) : Type := match b with | false => Nat | true => String def foo (b: Bool) : FooRetType b := match b with | false => (1 : Nat) | true => "hello" #eval foo true #eval foo false

index signature インデックス型： {[k : T] : S} の形で書ける型 いや違う、オブジェクト型やマップ型のインデックス集合の型を index signature と言っているのかな。 indexed access 型： T[K] という二項の型演算、または型演算で作られる型。特定の型や…

digraph { logic[label="形式化された\n定義／公理／定理／証明"] ts[label="TypeScript\nプログラムコード"] js[label="JavaScript\nプログラムコード\n(不要)"] logic -> ts[label=" 人手で相互翻訳", dir=both] ts -> js[label=" トランスパイラが翻訳 "]…

And_intro And intro And_left And elim left And_right And elim right Or_inl Or intro left Or_inr Or intro right fun_OR_MAKE なぜか無い 後で定義 Or elim 特殊 Imp intro MP（不要だが） Imp elim trivial True intro EFQ False elim 不要 Not intro …

アロー関数とアロー〈二重矢印記号〉を使った関数空間型の記述 declareを使った外部環境の型宣言 オンライン・プレイグラウンド 対応： TypeScript 疑似言語 function theorem const evidence declare function axiomatic theorem declare const axiomatic e…

型と値は区別する必要がある。 計算と演算を区別するのは難しい。曖昧に区別されていることもあるが、混同して使っても差し支えない。 関数と計算は一応区別するが、ヘッド部（後述）の有る無しの違いしかないので、混同して使っても差し支えない。 型と型の…

テーゼ： 十分に強力な型システム／型チェッカーを持ったプログラミング言語は、証明記述／証明検証に使える。 型 命題 型変数 命題変数 型定数 命題定数 型構成子 命題結合子 型の値 命題の証拠 計算・関数 証明・定理 計算・関数のプロファイル 証明可能性…