blob: 4e416778a9a7b7387eb48c63d4b753b402b1485d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* Check enough reduction happens in the conclusion of an induction scheme *)
Lemma foo :
forall (P : nat -> Prop),
(forall n, P (S n)) ->
forall n,
(fun e =>
IsSucc e ->
P e) n.
Proof.
Admitted.
Theorem bar : forall n,
IsSucc n ->
True.
Proof.
intros.
Fail induction n using foo. (* was an anomaly *)
Admitted.
|
