def
- defは新しい定義を作る命令
- defは次のように書く
Plaintext
def 名前 引数 : 返り値の型 :=
定義の中身Plaintext
def myFrobeniusFun (x : K) : K :=
x ^ p
/-
myFrobeniusFunを次のように定義する。
Kの元xを受け取り、Kの元x ^ pを返す。
-/ラムダ式を使って次のようにも書ける
Plaintext
def myFrobeniusFun : K → K :=
fun x => x ^ p通常の関数としてのdef
Plaintext
def 関数名 (引数 : 型) : 戻り値の型 :=
関数の中身Plaintext
def double (n : Nat) : Nat :=
n * 2通常の関数としてのdef
Lean4の関連記事
- 【Lean4】namespace
- 【Lean4】section
- 【Lean4】variable
- 【Lean4】abbrev
- 【Lean4】constructor
- 【Lean4】#check
- 【Lean4】def
- 【Lean4】exact
- 【Lean4】rfl
- 【Lean4】intro
- 【Lean4】apply
- 【Lean4】unfold
- 【Lean4】rw
- 【Lean4】simp
- 【Lean4】simpa
- 【Lean4】constructor
- 【Lean4】left,right
- 【Lean4】cases
- 【Lean4】rcases
- 【Lean4】refine
- 【Lean4】use
- 【Lean4】have
- 【Lean4】show
- 【Lean4】change
- 【Lean4】subst
- 【Lean4】by_cases
- 【Lean4】induction
- 【Lean4】ext
- 【Lean4】funext
- 【Lean4】congrArg
- 【Lean4】norm_num
- 【Lean4】ring
- 【Lean4】linarith
- 【Lean4】aesop
- 【Lean4】structure
- 【Lean4】where
- 【Lean4】@[simp]
- 【Lean4】 #eval
- 【Lean4】let
- 【Lean4】if（条件分岐）
- 【Lean4】match（パターンマッチ）
- 【Lean4】リスト
- 【Lean4】Option
- 【Lean4】inductive
