diff options
Diffstat (limited to 'test-suite/output/RecordProjParameter.out')
| -rw-r--r-- | test-suite/output/RecordProjParameter.out | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/output/RecordProjParameter.out b/test-suite/output/RecordProjParameter.out new file mode 100644 index 0000000000..91ae4b6511 --- /dev/null +++ b/test-suite/output/RecordProjParameter.out @@ -0,0 +1,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 |