2023-02-13から1日間の記事一覧
Coqの宇宙は {Set, Prop} → Type → Type → ... Leanの宇宙は Prop → Type → Type → ...Typeには番号が付く。別にどっちでもいい。圏論的には次の圏を準備する。$`\newcommand{\mrm}[1]{\mathrm{#1}} `$ $`{\bf Ded}`$ $`{\bf Set}`$ $`{\bf SET}`$ $`{\bf CA…
入力法は、コマンド "lean4: Show all abbribiations" で表示される。 文字 名前 番号 入力法 用途 “λ” Greek Small Letter Lamda U+03BB \lam ラムダ抽象 “↦” Rightwards Arrow from Bar U+21A6 \map ラムダ抽象の区切り “·” Middle Dot U+00B7 \. 無名ラム…
def main (args : List String) : IO UInt32 := doimport Mathlib.Tactic.LibrarySearch #check library_search%パーセント記号は相変わらず意味不明。名前短縮とは、修飾名を短くすること。ひとつは、open でカレント名前空間に別名前空間の名前をぶちまけ…
