lean2/tests/lean/backward_rule1.lean.expected.out

constant H [intro] : A → B
constant G [intro] : A → B → C
constant f [intro] : T → A
f
G
H
exists_unique.intro
Exists.intro
feat(library/attribute_manager, frontends/lean/builtin_cmds): use attribute manager information when pretty print definitions 2015-12-18 05:16:31 +00:00			`constant H [intro] : A → B`
			`constant G [intro] : A → B → C`
			`constant f [intro] : T → A`
refactor(library/blast/backward): use priority_queue, make sure head is normalized when building index 2015-12-28 20:10:56 +00:00			`f`
			`G`
			`H`
			`exists_unique.intro`
			`Exists.intro`