diff options
Diffstat (limited to 'test-suite/bugs/closed/3825.v')
| -rw-r--r-- | test-suite/bugs/closed/3825.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v index e594b74b6..666c64631 100644 --- a/test-suite/bugs/closed/3825.v +++ b/test-suite/bugs/closed/3825.v @@ -14,3 +14,11 @@ 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}. + |