lean2/tests/lean/pp.lean.expected.out

λ {A} B a b, a : Π B, ?A → B → ?A
λ {A B} a b, a : ?A → ?B → ?A
λ A {B} a b, a : Π A {B}, A → B → A
λ A B a b, a : Π A B, A → B → A
λ [A] B a b, a : Π B, ?A → B → ?A
λ ⦃A⦄ {B} a b, a : Π ⦃A⦄ {B}, A → B → A
λ ⦃A B⦄ a b, a : Π ⦃A B⦄, A → B → A
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`λ {A} B a b, a : Π B, ?A → B → ?A`
			`λ {A B} a b, a : ?A → ?B → ?A`
			`λ A {B} a b, a : Π A {B}, A → B → A`
			`λ A B a b, a : Π A B, A → B → A`
			`λ [A] B a b, a : Π B, ?A → B → ?A`
			`λ ⦃A⦄ {B} a b, a : Π ⦃A⦄ {B}, A → B → A`
			`λ ⦃A B⦄ a b, a : Π ⦃A B⦄, A → B → A`