`def`¶

def は計算内容をもつ定義を作るコマンドです．関数，値，命題の略記などを定義できます． def name : T := t は，「name という名前に，型 T の項 t を結びつける」と読みます．

def addTwo (n : Nat) : Nat :=
  n + 2

example : addTwo 3 = 5 := by
  rfl

def IsPositiveNat (n : Nat) : Prop :=
  0 < n

example : IsPositiveNat 3 := by
  unfold IsPositiveNat
  decide

def で定義した名前は，必要に応じて展開されます． rfl で証明できる等式は，定義を展開して両辺が同じ形になる等式です．この「定義を展開して同じになる」という同一性を，定義的な等しさと呼びます． def で関数を定義すると，その計算規則を rfl や simp が利用できることがあります．

example : addTwo 0 = 2 := by
  rfl

def¶

`def`¶