blob: cc85a764be664c12f1ad34394fc707ca5cf0b898 (
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
32
|
# Script simulating a dialog between coqide and coqtop -ideslave
# Run it via fake_ide
#
# Bug 2082
# Broken due to proof engine rewriting
#
INTERP Variable A : Prop.
INTERP Variable B : Prop.
INTERP Axiom OR : A \/ B.
INTERP Lemma MyLemma2 : True.
INTERP proof.
INTERP per cases of (A \/ B) by OR.
INTERP suppose A.
INTERP then (1 = 1).
INTERP then H1 : thesis.
INTERP thus thesis by H1.
INTERP suppose B.
REWIND 1
# <replay>
INTERP suppose B.
# </replay>
REWIND 2
# <replay>
INTERP thus thesis by H1.
INTERP suppose B.
# </replay>
INTERP then (1 = 1).
INTERP then H2 : thesis.
INTERP thus thesis by H2.
INTERP end cases.
INTERP end proof.
INTERP Qed.
|
