【Lean4】inductive

inductive

自分で型を作ることができる

Plaintext

inductive Color where
  | red
  | green
  | blue
  
def colorName (c : Color) : String :=
  match c with
  | Color.red => "red"
  | Color.green => "green"
  | Color.blue => "blue"

inductive Color where
  | red
  | green
  | blue
  
def colorName (c : Color) : String :=
  match c with
  | Color.red => "red"
  | Color.green => "green"
  | Color.blue => "blue"

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