blob: a4a35003df7c1827bf5d51311cc0e5b5336595a9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
Require Extraction.
Require Import List.
Section Test.
Variable A : Type.
Variable decA : forall (x y:A), {x=y}+{x<>y}.
(** Should fail when no proofs are started *)
Fail Show Extraction.
Lemma decListA : forall (xs ys : list A), {xs=ys}+{xs<>ys}.
Proof.
Show Extraction.
fix decListA 1.
destruct xs as [|x xs], ys as [|y ys].
Show Extraction.
- now left.
- now right.
- now right.
- Show Extraction.
destruct (decA x y).
+ destruct (decListA xs ys).
* left; now f_equal.
* Show Extraction.
right. congruence.
+ right. congruence.
Show Extraction.
Defined.
End Test.
|
