帰納的型
帰納的型(inductive type)
型がどういうものかを定義する感じのもの
1. 構成規則 (formation rule)
2. 構成子 (constructor)
3. 除去子 (eliminator)
4. 計算規則 (computation rule)
Coqの帰納型は以下のような記法
code:coq
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
Lean4の場合
code:Lean4
inductive <型名> : Type
| <要素1> : <型名>
| <要素2> : <型名>
:
| <要素N> : <型名>
これは列挙型
code:Lean4
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
確認用
Q. 帰納型
関連
参考
メモ
Coq
Lean 4