lean2/tests/lean/auto_include.lean.expected.out

definition foo : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
λ A _inst_1 a b, sorry
definition bla : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
λ B _inst_2 b, sorry
definition foo2 : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
λ A _inst_1 a b, sorry
definition bla2 : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
λ B _inst_2 b, sorry
feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included) 2015-12-13 21:20:07 +00:00			`definition foo : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`λ A _inst_1 a b, sorry`
feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included) 2015-12-13 21:20:07 +00:00			`definition bla : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`λ B _inst_2 b, sorry`
feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included) 2015-12-13 21:20:07 +00:00			`definition foo2 : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`λ A _inst_1 a b, sorry`
feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included) 2015-12-13 21:20:07 +00:00			`definition bla2 : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`λ B _inst_2 b, sorry`