michael/lean2 - Forgejo: Beyond coding. We forge.

michael/lean2

12 lines

175 B

Text

Raw Permalink Normal View History

-												test(tests/lean/extra): add test for "show goal" feature

											
										
										
											2015-07-28 03:59:29 +00:00
+								LEAN_INFORMATION
-												fix(frontends/lean): "show goal" localization, add "position", support "by tactic"

											
										
										
											2015-07-28 18:06:27 +00:00
+								position 20:4
-												test(tests/lean/extra): add test for "show goal" feature

											
										
										
											2015-07-28 03:59:29 +00:00
+								a b c d : ℕ,
 								h₁ : a + b = 0,
 								h₂ : b = 0,
 								aeq0 : a = 0,
 								h₃ : c + 1 + a = 1,
 								h₄ : d = c - 1,
 								ceq : c = 0
 								⊢ d = 0
 								END_LEAN_INFORMATION