what does . mean here?

Stream: new members

[Bryan Gin-ge Chen]

I copied this from library/init/data/nat/basic.lean.

lemma not_succ_le_zero : ∀ (n : ℕ), nat.succ n ≤ 0 → false
.

[cbailey]

It's syntax to execute a method inside a module (the nat module). If you do

open nat

you can access succ without the nat. prefix by opening the nat namespace. There's a section in "Theorem Proving in Lean" about the module/namespace keywords.

[Bryan Gin-ge Chen]

Sorry, I meant the . on the line all by itself, which somehow suffices as a proof of this lemma.

[Patrick Massot]

Usually an dot at the end of something is there only to help the parser

[Bryan Gin-ge Chen]

What do you mean by "help the parser" here? Is the dot shorthand for something?

[Patrick Massot]

I mean it tells the parser that something ends here.

[Patrick Massot]

But really I don't know why there is something to end here. The statement is trivial but many other trivial things still require a proof

[Rob Lewis]

It's being used to indicate that this is an empty pattern match. Structurally, there's no n for which you can have a proof of succ n ≤ 0.

[Rob Lewis]

So you're proving the lemma by induction on n, except there are no cases because none of them make sense.

[Rob Lewis]

You need the . so that Lean knows the proof is over and doesn't confuse the next line with a continuation of the lemma statement.

[Bryan Gin-ge Chen]

OK, that makes sense, thanks!

[cbailey]

Oh I was way off lol. My apologies.