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

michael/lean2

8 lines

139 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 7:2
-												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
 								⊢ c + 1 + a = 1 → d = c - 1 → d = 0
 								END_LEAN_INFORMATION