29 lines
558 B
Text
29 lines
558 B
Text
|
inductive nat : Type :=
|
||
|
|
| zero : nat
|
||
|
|
| succ : nat → nat
|
||
|
|
|
||
|
|
inductive list (A : Type) : Type :=
|
||
|
|
| nil : list A
|
||
|
|
| cons : A → list A → list A
|
||
|
|
|
||
|
|
check nil
|
||
|
|
check nil.{1}
|
||
|
|
check @nil.{1} nat
|
||
|
|
check @nil nat
|
||
|
|
|
||
|
|
check cons zero nil
|
||
|
|
|
||
|
|
inductive vector (A : Type) : nat → Type :=
|
||
|
|
| vnil : vector A zero
|
||
|
|
| vcons : forall {n : nat}, A → vector A n → vector A (succ n)
|
||
|
|
|
||
|
|
check vcons zero vnil
|
||
|
|
variable n : nat
|
||
|
|
check vcons n vnil
|
||
|
|
|
||
|
|
check vector_rec
|
||
|
|
|
||
|
|
definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
|
||
|
|
:= vector_rec nil (fun n a v l, cons a l) v
|
||
|
|
|