9 lines
110 B
Text
9 lines
110 B
Text
variable {A : Type}
|
|
|
|
check @id
|
|
|
|
inductive list :=
|
|
| nil : list
|
|
| cons : A → list → list
|
|
|
|
check @list.cons
|