## Stream: new members

### Topic: Magic dot in place of proof?

#### 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?

#### 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!

magic. :-)

#### 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.

#### 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

#### Mark Dickinson (Nov 05 2018 at 21:59):

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

#### Patrick Massot (Nov 05 2018 at 21:59):

And there are very few opportunities to use this trick

No problem

#### 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 ..

#### Kevin Buzzard (Nov 05 2018 at 23:40):

I usually insert a #exit

Last updated: May 14 2021 at 07:19 UTC