blob: 8b892c694c2df7f149d77e928dbc3882ff98d4c2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Record Atype : Type :=
{ t1 : forall (a : Type), a
; t2 : Type
; t3 : t2 }.
About t1.
About t3.
Record Btype : Type :=
{ u1 : forall (b : Type) (b0 : Type), b * b0
; u2 : Type
; u3 : u2 }.
About u1.
About u3.
Record Ctype : Type :=
{ v1 : forall (c0 : Type), c0
; v2 : Type
; v3 : v2
}.
About v1.
About v3.
|
