diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-17 23:48:21 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
commit | 4940f99922b0784d726b7c50abe63395713f012f (patch) | |
tree | 750124bae7b6a575d98b9cfe439c798c555fc531 /test-suite/output | |
parent | f8e639f3b81ae142f5b529be1ad90210fc259375 (diff) |
Fix #5347: unify declaration of axioms with and without bound univs.
Note that this makes the following syntax valid:
Axiom foo@{i} bar : Type@{i}.
(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
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. |