lean2/tests/lean/interactive/proof_state_info3.input
2015-03-27 17:54:48 -07:00

19 lines
No EOL
222 B
Text

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