lean2/tests/lean/584a.lean.expected.out

foo : Π A [H], A → A
foo' : Π {A} [H] {x}, A
foo ℕ 10 : ℕ
definition test : ∀ {A : Type} [H : inhabited A], @foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5) = 10 :=
λ A H, @rfl ℕ (@foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5))
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								foo : Π A [H], A → A
 								foo' : Π {A} [H] {x}, A
-												fix(frontends/lean/parser): fixes #584

											
										
										
											2015-05-07 21:24:30 +00:00
+								foo ℕ 10 : ℕ
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								definition test : ∀ {A : Type} [H : inhabited A], @foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5) = 10 :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ A H, @rfl ℕ (@foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5))