Stream: new members
Claus-Peter Becke (Aug 21 2020 at 07:36):
I tried to prove the lemma in the Natural Number Game in Inequation World level 7 with the following tactics:
cases h with c ha, symmetry at ha, have h2 := add_right_eq_zero ha if ha : a + c = 0, exact h2,
All goals were closed. But there remained the following error messages:
Messages 20:32: error: invalid 'begin-end' expression, ',' expected 21:0: error: sync
I don't know which operations cause the messages and what I can do to avoid them? Does anybody have an explanation and a hint?
Shing Tak Lam (Aug 21 2020 at 07:41):
I think the issue is to do with the
if there. Notice the "if" in the message on the top is not monospace (ie not code)
Claus-Peter Becke (Aug 21 2020 at 07:45):
Thank you for that hint. So I will have a closer look on the if to find the causes for this error message.
Kevin Buzzard (Aug 21 2020 at 07:45):
Kevin Buzzard (Aug 21 2020 at 07:46):
Yeah that definition of h2 doesn't make any sense to Lean
Claus-Peter Becke (Aug 21 2020 at 07:52):
At the first attempt I obviously followed too directly the explanations and hints in level 7 in Inequality World. In the meantime I substituted the line containing the have-tactic by the following one:
That works fine.
Claus-Peter Becke (Aug 21 2020 at 07:53):
exact add_right_eq_zero ha
Last updated: May 16 2021 at 05:21 UTC