def f1 (n:Nat) (m:Nat) : Nat := n + m def f2 (n:Nat) : Nat → Nat := fun (m:Nat) => n + m def f3 : Nat → Nat → Nat := fun (n :Nat) => fun(m:Nat) => n + m def f4 : Nat → Nat → Nat := fun (n m:Nat) => n + m #check f1 #check f2 #check f3 #chec…

problem Γ ok? （コンテキスト Γ は正しいか？） judgement Γ ok （コンテキスト Γ は正しい） problem Γ |- t ok? （項 t は、コンテキスト Γ で解釈できるか？） judgementm Γ |- t ok （項 t は、コンテキスト Γ で解釈できる） problem Γ |- ?t : A （型…

wt.exe が2箇所にあった。 C:\Users\m-hiyama\AppData\Local\Microsoft\WindowsApps\wt.exe C:\Program Files\WindowsApps\Microsoft.WindowsTerminal_1.15.3466.0_x64__8wekyb3d8bbwe\wt.exe が、C:\Users\m-hiyama\AppData\Local\Microsoft\WindowsApps\wt…

命題は型である。← そんなわけないだろ。 命題は型の一種である。 [間違い] 命題はデータ型の一種である。 命題とデータ型は違う。が、命題は型の一種である。 命題は広義の型の一種である。 命題は広義の型の一種であり、データ型も広義の型の一種である。 …

矢印の奪い合い問題 含意を表す 指数型〈関数型 | アロー型〉を表す 射のプロファイルの区切り記号 シーケントの区切り記号（前提と結論） 暫定的解決 含意と指数はカリー／ハワード対応により同一視して → を使う。 射のプロファイルの区切り記号にターンス…

「CTRL+ALT+P」で Powershell だったのだが、この設定は： [Win]+[Q] から Powershell を探す。 [ファイルの場所を開く] でディレクトリを見る。 "Windows Powershell" がリンクになっているので、プロパティを見る。 プロパティのショートカットキー項目に…

久しぶりで色々忘れている。 MSYS2のルート / は C:\msys64\ MSYS2の /c/ は C:\ したがって、/c/msys64/ は / /ucrt64/, /mingw64/, /clang64/ と、それらの32ビット版があるが、当初はダミーで空っぽ clang32.exe, clangarm64.exe, mingw64.exe, ucrt64.ex…