【Lean4】match（パターンマッチ）

match

値の形によって処理を分ける

Plaintext

def describeNat (n : Nat) : String :=
  match n with
  | 0 => "zero"
  | 1 => "one"
  | _ => "larger" -- | _ は「それ以外」を表す

#eval describeNat 0
#eval describeNat 1
#eval describeNat 10

def describeNat (n : Nat) : String :=
  match n with
  | 0 => "zero"
  | 1 => "one"
  | _ => "larger" -- | _ は「それ以外」を表す

#eval describeNat 0
#eval describeNat 1
#eval describeNat 10

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