Lean4

inductive自分で型を作ることができるPlaintextinductive Color where | red | green | blue def colorName (c : Color) : String := match c ...

Option値が存在するかもしれないし、存在しないかもしれない場合に使うPlaintextdef safeHead (xs : List Nat) : Option Nat := match xs with | [] => none | x...

リストリストは同じ型の値を並べたものPlaintextdef numbers : List Nat := [1, 2, 3, 4]def numbers : List Nat := [1, 2, 3, 4]

match値の形によって処理を分けるPlaintextdef describeNat (n : Nat) : String := match n with | 0 => "zero" | 1 => "one" | _ => "larger"...

if … then … else …は条件分岐Plaintextdef isZeroMessage (n : Nat) : String := if n == 0 then "zero" else "not zero"def isZeroM...

let関数の中で一時的な値を作るPlaintextdef squarePlusOne (n : Nat) : Nat := let square := n * n square + 1#eval squarePlusOne 4/-17-/d...

#eval#eval：実際に計算して結果を表示するPlaintextdef double (n : Nat) : Nat := n * 2#eval double 5/-10-/def double (n : Nat) : Nat := n...

@この定理をsimpが自動的に使ってよい規則として登録する指定

where「この型の構造を、以下のフィールドを指定して作ります」という意味 Plaintextdef 名前 : 構造の型 where フィールド1 := 値1 フィールド2 := 値2 ...def 名前 : 構造の型 where フィール...

structure複数のデータや証明をまとめたものをstructureと呼ぶ