src/Init/Notation.lean からの情報。構文範疇precは項の優先度を表す値（の表現）のことで： 項の優先度： max = 1024, arg = 1023, lead = 1022, min = 10 パイプ記号 は優先度は min = 10 =, ∈ が50 足し算は65、 規表現風接尾辞の *,+,? は arg = 1023 S…

演算子優先度〈prec〉は適切かどうかわからない。 infix:70 "←" => Nat.pow #eval 5 ← 2 -- 25 def sqPow (n:Nat) : Nat := n ← (n * n) #eval sqPow 2 -- 16

Idris 2で次のコードを書けるようだ。 def typeDesc (ty : Type) : String := match ty with | Int => "integer" | String => "string" | List α => "list of " ++ typeDesc α | _ => "something else"Leanでは無理だ。パターンマッチ match/withが帰納的集…

proof ... end {theorem | lemma} 名前 : 前提リスト |- 結論 proof ... end {fact | rule} 名前 : 前提リスト |- 結論 we have ラベル : 命題 from 証明項 we have ラベル : 命題 （前提または直前の結果から） we have 命題 {from 証明項}? （ラベルは thi…