Zulip Chat Archive

Stream: new members

Topic: le_zero


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 07:45):

(deleted)

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 07:46):

Yeah that definition of h2 doesn't make any sense to Lean

view this post on Zulip 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.

view this post on Zulip Claus-Peter Becke (Aug 21 2020 at 07:53):

exact add_right_eq_zero ha

Last updated: May 16 2021 at 05:21 UTC