lean2/tests/lean/extra/755.expected.out

LEAN_INFORMATION
position 55:52
A : Type,
B : Type,
f : one_step_tr A → B
⊢ Π x y,
    f (tr x) = f (tr y)
END_LEAN_INFORMATION
fix(frontends/lean/elaborator): fixes #755 2015-07-29 23:28:48 +00:00			`LEAN_INFORMATION`
			`position 55:52`
			`A : Type,`
			`B : Type,`
			`f : one_step_tr A → B`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`⊢ Π x y,`
fix(frontends/lean/elaborator): fixes #755 2015-07-29 23:28:48 +00:00			`f (tr x) = f (tr y)`
			`END_LEAN_INFORMATION`