File: bug_3825.v

package info (click to toggle)
coq-doc 8.20.0-2
  • links: PTS, VCS
  • area: non-free
  • in suites: forky, sid, trixie
  • size: 46,708 kB
  • sloc: ml: 234,429; sh: 4,686; python: 3,359; ansic: 2,644; makefile: 842; lisp: 172; javascript: 87; xml: 24; sed: 2
file content (23 lines) | stat: -rw-r--r-- 395 bytes parent folder | download | duplicates (5) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
 
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}.