blob: 8656ff1a3944de94ccd08b195a936beec172df6f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Set Universe Polymorphism.
Set Printing Universes.
Unset Strict Universe Declaration.
Class Wrap A := wrap : A.
Instance bar@{u} : Wrap@{u} Set. Proof nat.
Print bar.
(* The universes in the binder come first, then the extra universes in
order of appearance. *)
Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
Print foo.
|
