diff options
Diffstat (limited to 'test-suite/bugs/closed/3825.v')
-rw-r--r-- | test-suite/bugs/closed/3825.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v new file mode 100644 index 00000000..666c6463 --- /dev/null +++ b/test-suite/bugs/closed/3825.v @@ -0,0 +1,24 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Axiom foo@{i j} : Type@{i} -> Type@{j}. + +Notation bar := foo. + +Monomorphic Universes i j. + +Check bar@{i j}. +Fail Check bar@{i}. + +Notation qux := (nat -> nat). + +Fail Check qux@{i}. + +Axiom TruncType@{i} : nat -> Type@{i}. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (0)-Type. + +Check hProp. +Check hProp@{i}. + |