Leanのfun - mrsekut-p

Leanのfun

λ

無名関数を定義する

https://aconite-ac.github.io/theorem_proving_in_lean4_ja/dependent_type_theory.html#function-abstraction-and-evaluation-関数抽象と評価

code:lean

#check fun x : Nat => x + 5

#check λ x : Nat => x + 5

以下同じ

code:lean

#check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2

#check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2

#check fun x y => if not y then x + 1 else x + 2 -- Nat → Bool → Nat