Leanのdef

項の定義

項とは、変数、関数、型そのものなど

tsのconstに近いmrsekut.icon

例

変数

code:lean(ts)

def m : Nat := 1 -- m は自然数型を持つ

def b2 : Bool := false

関数

ref

code:lean

def double (x : Nat) : Nat :=

x + x

型

ref

code:lean(ts)

def α : Type := Nat

def F : Type → Type := List

型も変数も同じキーワードで定義するんやねmrsekut.icon

typescriptだとconstとtypeのように別物を使うが

()ではなく{}を使って引数を囲うことで、型引数をデフォルトで推論させられる

依存型理論 - Theorem Proving in Lean 4 日本語訳

cons関数は以下のように定義できる

通常の書き方

code:①

def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α :=

List.cons a as

{}を使ったもの

code:②

def Lst.cons {α : Type u} (a : α) (as : Lst α) : Lst α :=

List.cons a as

②をLeanのvariableを使って書いたもの

code:②'

section

variable {α : Type u}

def Lst.cons (a : α) (as : Lst α) : Lst α := List.cons a as

end

①のように定義すると、使用時に毎回型を指定しないといけなくて面倒

code:lean

#check Lst.cons Nat 5 (Lst.nil Nat) -- Lst Nat

code:lean

#check Lst.cons _ 5 (Lst.nil _) -- Lst Nat

_でholeを作れるが、それでも面倒

②や②'のように{}を使って型を囲うと、使用時に省略して書ける

code:lean

#check Lst.cons 5 Lst.nil

逆に、普通に型を書くとエラーになる

code:lean

#check Lst.cons Nat 5 (Lst.nil Nat) -- error

#check Lst.cons _ 5 (Lst.nil _) -- error

明示的に型を指定する場合は

こうするか

code:lean

#check Lst.cons (5:Nat) Lst.nil

@関数名型を使って、こうも書ける

code:lean

#check @Lst.cons Nat 5 Lst.nil

こういう部分適用ができるイメージmrsekut.icon

code:lean

def nat_cons := @Lst.cons Nat