blob: ef219973df71904dde56e9dac67851b0a6f285d8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Inductive foo (V:Type):Type :=
| Foo : list (bar V) -> foo V
with bar (V:Type): Type :=
| bar1: bar V
| bar2 : V -> bar V.
Module WithPoly.
Polymorphic Inductive foo (V:Type):Type :=
| Foo : list (bar V) -> foo V
with bar (V:Type): Type :=
| bar1: bar V
| bar2 : V -> bar V.
End WithPoly.
|
