Zulip Chat Archive

Stream: new members

Topic: Magic dot in place of proof?


view this post on Zulip Mark Dickinson (Nov 05 2018 at 21:50):

Looking through the standard library, I see this in basic.lean:

lemma not_succ_le_zero :  (n : ), succ n  0  false
.

What's the magic dot on the second line? Is this syntactic sugar for a particular tactic or set of tactics?

Source : https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/library/init/data/nat/basic.lean#L84-L85

view this post on Zulip Scott Morrison (Nov 05 2018 at 21:51):

no, it just says "this is the end of the definition", and causes lean to realise that there are no cases to prove!

view this post on Zulip Scott Morrison (Nov 05 2018 at 21:51):

magic. :-)

view this post on Zulip Patrick Massot (Nov 05 2018 at 21:56):

See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/what.20does.20.2E.20mean.20here.3F

view this post on Zulip Mark Dickinson (Nov 05 2018 at 21:58):

Ah, thank you! I did try searching the archives, but it's not easy to figure out how to search for a single period.

view this post on Zulip Patrick Massot (Nov 05 2018 at 21:59):

I searched for the name of this lemma, because I was pretty sure it was already discussed

view this post on Zulip Mark Dickinson (Nov 05 2018 at 21:59):

Yep, I should have thought to use not_succ_le_zero as a search term ..

view this post on Zulip Patrick Massot (Nov 05 2018 at 21:59):

And there are very few opportunities to use this trick

view this post on Zulip Patrick Massot (Nov 05 2018 at 21:59):

No problem

view this post on Zulip Bryan Gin-ge Chen (Nov 05 2018 at 23:37):

I've sometimes found it useful when rewriting a proof, e.g. instead of temporarily commenting out the rest of a proof, I just insert a ..

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 23:40):

I usually insert a #exit


Last updated: May 14 2021 at 07:19 UTC