blob: e06998b71177014fa180c68ef5fe967929f6eb35 (
plain)
1
2
3
4
5
6
7
8
|
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.
|
