unfold
定義を展開する
Plaintext
def double (n : ℕ) : ℕ :=
n + n
example (n : ℕ) : double n = n + n := by
unfold doubleLean4の関連記事
- 【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
