diff options
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/UnivBinders.out | 24 | ||||
-rw-r--r-- | test-suite/output/UnivBinders.v | 13 |
2 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 9eb162fc0..f69379a57 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -129,3 +129,27 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic +axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i} +(* i Top.33 Top.34 |= *) + +axfoo is universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axfoo +axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i} +(* i Top.33 Top.34 |= *) + +axbar is universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axbar +axfoo' : Type@{Top.36} -> Type@{i} + +axfoo' is not universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axfoo' +axbar' : Type@{Top.36} -> Type@{i} + +axbar' is not universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axbar' +The command has indeed failed with message: +When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index a65a1fdf3..116d5e5e9 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -86,3 +86,16 @@ Module SomeFunct (In : SomeTyp). End SomeFunct. Module Applied := SomeFunct(SomeMod). Print Applied.infunct. + +(* Multi-axiom declaration + + In polymorphic mode the domain Type gets separate universes for the + different axioms, but all axioms have to declare all universes. In + polymorphic mode they get the same universes, ie the type is only + interpd once. *) +Axiom axfoo@{i+} axbar : Type -> Type@{i}. +Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}. + +About axfoo. About axbar. About axfoo'. About axbar'. + +Fail Axiom failfoo failbar@{i} : Type. |