Magic dot in place of proof?

Stream: new members

[Mark Dickinson]

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

[Scott Morrison]

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

[Scott Morrison]

magic. :-)

[Patrick Massot]

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

[Mark Dickinson]

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]

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

[Mark Dickinson]

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

[Patrick Massot]

And there are very few opportunities to use this trick

[Patrick Massot]

No problem

[Bryan Gin-ge Chen]

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]

I usually insert a #exit