## Stream: new members

### Topic: what does . mean here?

#### Bryan Gin-ge Chen (Aug 30 2018 at 14:26):

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

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


#### cbailey (Aug 30 2018 at 14:29):

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 (Aug 30 2018 at 14:30):

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

#### Patrick Massot (Aug 30 2018 at 14:31):

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

#### Bryan Gin-ge Chen (Aug 30 2018 at 14:38):

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

#### Patrick Massot (Aug 30 2018 at 14:39):

I mean it tells the parser that something ends here.

#### Patrick Massot (Aug 30 2018 at 14:39):

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 (Aug 30 2018 at 14:41):

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 (Aug 30 2018 at 14:41):

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

#### Rob Lewis (Aug 30 2018 at 14:42):

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 (Aug 30 2018 at 14:42):

OK, that makes sense, thanks!

#### cbailey (Aug 30 2018 at 14:49):

Oh I was way off lol. My apologies.

Last updated: May 13 2021 at 22:15 UTC