lean2/tests/lean/interactive/info.input.expected.out

-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- TYPE|6|8
?a → ?b → ?a ∧ ?b
-- ACK
-- IDENTIFIER|6|8
and.intro
-- ACK
-- ENDINFO
-- BEGININFO
-- SYMBOL|7|8
(
-- ACK
-- TYPE|7|9
a ∧ b → b
-- ACK
-- IDENTIFIER|7|9
and.elim_right
-- ACK
-- TYPE|7|24
a ∧ b
-- ACK
-- IDENTIFIER|7|24
H
-- ACK
-- ENDINFO
fix(frontends/lean/info_manager): std::set insert is a noop if set already contains an equivalent element 2014-10-30 10:33:38 -07:00			`-- BEGINWAIT`
			`-- ENDWAIT`
			`-- BEGININFO`
			`-- TYPE\|6\|8`
feat(frontends/lean): `lean --server` should display meta-variables using the approach used in check command, closes #280 2014-10-30 12:45:41 -07:00			`?a → ?b → ?a ∧ ?b`
fix(frontends/lean/info_manager): std::set insert is a noop if set already contains an equivalent element 2014-10-30 10:33:38 -07:00			`-- ACK`
			`-- IDENTIFIER\|6\|8`
			`and.intro`
			`-- ACK`
			`-- ENDINFO`
			`-- BEGININFO`
			`-- SYMBOL\|7\|8`
			`(`
			`-- ACK`
			`-- TYPE\|7\|9`
			`a ∧ b → b`
			`-- ACK`
			`-- IDENTIFIER\|7\|9`
			`and.elim_right`
			`-- ACK`
			`-- TYPE\|7\|24`
			`a ∧ b`
			`-- ACK`
			`-- IDENTIFIER\|7\|24`
			`H`
			`-- ACK`
			`-- ENDINFO`