michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lean/interactive): add test for proof_state info

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-29 16:44:10 -08:00
parent c74da8bea2
commit e9d8a960d9
2 changed files with 49 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
tests/lean/interactive/proof_state_info3.input Normal file
View file

@ -0,0 +1,19 @@
VISIT proof_state_info3.lean
SYNC 11
theorem tst (a b c : Prop) : a → b → a ∧ b :=
begin
info,
intros (Ha, Hb),
info,
apply and.intro,
apply Ha,
apply Hb,
end
WAIT
REPLACE 7
state,
SHOW
WAIT
INFO 8 17

30
tests/lean/interactive/proof_state_info3.input.expected.out Normal file
View file

@ -0,0 +1,30 @@
-- BEGINWAIT
-- ENDWAIT
-- BEGINSHOW
theorem tst (a b c : Prop) : a → b → a ∧ b :=
begin
info,
intros (Ha, Hb),
state,
apply and.intro,
apply Ha,
apply Hb,
end
-- ENDSHOW
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- PROOF_STATE|8|17
a b c : Prop,
Ha : a,
Hb : b
⊢ a
--
a b c : Prop,
Ha : a,
Hb : b
⊢ b
-- ACK
-- ENDINFO