blob: 79633f4893a4240e43e31b4aa42a836c6b09f701 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* Checking typability of intermediate return predicates in nested pattern-matching *)
Inductive A : (Type->Type) -> Type := J : A (fun x => x).
Definition ret (x : nat * A (fun x => x))
:= match x return Type with
| (y,z) => match z in A f return f Type with
| J => bool
end
end.
Definition foo : forall x, ret x.
Proof.
Fail refine (fun x
=> match x return ret x with
| (y,J) => true
end
).
|
