Lean 4 Notes
CS 99: Functional Programming and Theorem Proving in Lean 4
Functional Programming
Currying
def curry (x : Nat) (y : Nat) : Nat := x + y + 1
def add := curry 1
#check add
-- add (y : Nat) : Nat
def f := List.map String.length
#eval f ["123"]
-- [3]
Inductives
Recursive Inductive
inductive FakeNat where
| zero
| succ (n : FakeNat)
def toNat : FakeNat → Nat
| .zero => 0
| .succ n => 1 + toNat n
#eval FakeNat.zero
#eval toNat FakeNat.zero.succ.succ
Strict Positivity: 不是函数的参数
inductive Bad where
| bad (f : Bad → Nat)
-- (kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declared
就是如果这样定义的话，会造成无限向前递归的情况。