blob: 2a8b517bd438484ba65c3a8e6336bf9e4a758264 (
plain)
1
2
3
4
5
6
7
|
Require Import Hurkens.
Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
Definition unwrap' := fun (X : Type) (b : box X) => let (unwrap) := b in unwrap.
Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl.
|
