blob: 1e0b4dbf2336ac5f99e7d7c05e5102e77f9b4cd3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* The kernel may convert application arguments right to left,
resulting in ill-typed terms, but should be robust to them. *)
Inductive Hide := hide : forall A, A -> Hide.
Lemma foo : (hide Type Type) = (hide (nat -> Type) (fun x : nat => Type)).
Proof.
Fail reflexivity.
match goal with |- ?l = _ => exact_no_check (eq_refl l) end.
Fail Defined.
Abort.
Definition HideMore (_:Hide) := 0.
Definition foo : HideMore (hide Type Type) = HideMore (hide (nat -> Type) (fun x : nat => Type))
:= eq_refl.
|
