blob: 14b66db3623cb9e976b3ac0af734165c39d5988f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Set Universe Polymorphism.
Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
Inductive Empty : Type1 := .
Fail Check Empty : Set.
(* Toplevel input, characters 15-116:
Error: Conversion test raised an anomaly *)
(* Now we make sure it's not an anomaly *)
Goal True.
Proof.
try exact (let x := Empty : Set in I).
exact I.
Defined.
|
