blob: ee4a9b083a05d754504a957d3b7e3d9be48afcb9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* 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
).
Abort.
|
