blob: 10f955b41f708ba23aa4b4037665fb22089adb6f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Unset Primitive Projections.
Record Box (A:Type) := box { unbox : A }.
Arguments box {_} _. Arguments unbox {_} _.
Definition map {A B} (f:A -> B) x :=
match x with box x => box (f x) end.
Definition tuple (l : Box Type) : Type :=
match l with
| box x => x
end.
Fail Inductive stack : Type -> Type :=
| Stack T foos :
tuple (map stack foos) ->
stack T.
|
