blob: 91ae4b6511e051cb884c99501c45d92a2a72dca9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
t1 : Atype -> forall a : Type, a
t1 is not universe polymorphic
Arguments t1 _ _%type_scope
t1 is transparent
Expands to: Constant RecordProjParameter.t1
t3 : forall a0 : Atype, t2 a0
t3 is not universe polymorphic
t3 is transparent
Expands to: Constant RecordProjParameter.t3
u1 : Btype -> forall b b0 : Type, b * b0
u1 is not universe polymorphic
Arguments u1 _ (_ _)%type_scope
u1 is transparent
Expands to: Constant RecordProjParameter.u1
u3 : forall b1 : Btype, u2 b1
u3 is not universe polymorphic
u3 is transparent
Expands to: Constant RecordProjParameter.u3
v1 : Ctype -> forall c0 : Type, c0
v1 is not universe polymorphic
Arguments v1 _ _%type_scope
v1 is transparent
Expands to: Constant RecordProjParameter.v1
v3 : forall c : Ctype, v2 c
v3 is not universe polymorphic
v3 is transparent
Expands to: Constant RecordProjParameter.v3
|
