Zulip Chat Archive

Stream: new members

Topic: what does . mean here?


view this post on Zulip 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
.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 30 2018 at 14:31):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Aug 30 2018 at 14:39):

I mean it tells the parser that something ends here.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Aug 30 2018 at 14:42):

OK, that makes sense, thanks!

view this post on Zulip cbailey (Aug 30 2018 at 14:49):

Oh I was way off lol. My apologies.


Last updated: May 13 2021 at 22:15 UTC