Zulip Chat Archive

Stream: general

Topic: syntax surprises

Sebastian Ullrich (Jun 19 2018 at 11:10):

The Lean 4 parser only understands prelude, import, and theory so far, but I've already learned something surprising: noncomputable theory can be used anywhere in a file (also, multiple times)

Sean Leather (Jun 19 2018 at 11:16):

Can you elucidate on what is surprising about that?

Sebastian Ullrich (Jun 19 2018 at 11:28):

I assumed it only worked on the top of a file, since we usually use "theory" synonymously to "file".

Sean Leather (Jun 19 2018 at 11:43):

Ah, theory, not theorem: I missed that. I also didn't know theory was a keyword.

Sean Leather (Jun 19 2018 at 11:46):

I've only worked on computable theorems. Looking in the Lean 3 core library and mathlib, I see only noncomputable theory used. I don't see theory mentioned in the reference manual or TPIL. What purpose does theory serve?

Sebastian Ullrich (Jun 19 2018 at 11:50):

theory is a command, like theorem. noncomputable is a modifier you can apply to either of them. The distinction doesn't really matter in Lean 3 since theory can only be used together withnoncomputable, which marks the remainder of the file as noncomputable.

Kenny Lau (Jun 19 2018 at 11:51):

which marks the appropriate remainder of the file as noncomputable

Sebastian Ullrich (Jun 19 2018 at 11:51):

yes

Kenny Lau (Jun 19 2018 at 11:51):

computable functions remain computable

Sebastian Ullrich (Jun 19 2018 at 11:55):

Perhaps we'll want to generalize theory in Lean 4, though I'm not sure whether there are many sensible combinations. Say, using private theory, then negating it using a new keyword public on a few declarations.

Kenny Lau (Jun 19 2018 at 11:55):

lean -- java remade

Reid Barton (Jun 19 2018 at 13:32):

Oh funny, I've used noncomputable theory inside a section before and sort of expected it to be scoped, though there's no way I'd ever notice if it wasn't.

Johannes Hölzl (Jun 19 2018 at 14:40):

wasn't there a Github issue the idea of introducing also meta theory?

Johannes Hölzl (Jun 19 2018 at 14:42):

@Sebastian Ullrich what about changing theory to be only allowed at the file header, but extend section and namespace to take meta, noncomputable, private, protected, public modifiers?

Kenny Lau (Jun 19 2018 at 14:43):

how do you define file header?

Kenny Lau (Jun 19 2018 at 14:43):

currently import must be at the beginning

Sebastian Ullrich (Jun 19 2018 at 14:43):

@Johannes Hölzl Yes, that's my plan right now :)

Sebastian Ullrich (Jun 19 2018 at 14:43):

Also, attributes on sections

Johannes Hölzl (Jun 19 2018 at 14:43):

Nice!

Sebastian Ullrich (Jun 19 2018 at 14:45):

@Kenny Lau Right now I've defined it as prelude? (import ...)* (noncomputable theory)?

Kenny Lau (Jun 19 2018 at 14:46):

are you going to regex the whole file

Sebastian Ullrich (Jun 19 2018 at 14:46):

Of course, everyone knows you solve all problems with regexes

Kenny Lau (Jun 19 2018 at 14:47):

now you have 2...

Johannes Hölzl (Jun 19 2018 at 14:48):

modulo whitespace / comments

Sebastian Ullrich (Jun 19 2018 at 14:48):

repeat { all_goals { apply_regex } }

Johannes Hölzl (Jun 19 2018 at 14:55):

another purpose of theory could be to set parameters, or execute an imported command, like mathlib theory. This would setup certain notation, options, namespaces, version checks etc. I guess this could be also solved using run_cmd, but theory is a nice syntax. Also, what about moving prelude to prelude theory?

Sebastian Ullrich (Jun 19 2018 at 14:59):

prelude should logically come before import since it suppreses the default imports. We could move theory to the front instead, I'm not sure.

Johannes Hölzl (Jun 19 2018 at 15:02):

Okay, this makes sense.

Sebastian Ullrich (Jun 19 2018 at 15:04):

There shouldn't be any reason to restrict the modifiers applicable to theory in Lean 4, no. Though, in the examples so far, it sounded like applying something to theory or section simply distributes it to all contained declarations (even if, as Kenny pointed out, it will behave differently from e.g. an explicit noncomputable). Your mathlib example doesn't quite fit in that scheme.

Mario Carneiro (Jun 19 2018 at 15:37):

Will lean 4 allow for gathering the global file structure? For example: find the open section and namespace names; currently declared variables and parameters, notations and other local declarations; finding the "outline" of a given file, i.e. the tree of namespace and section blocks and the definitions in them

Sebastian Ullrich (Jun 19 2018 at 15:43):

You'll definitely get access to a concrete syntax tree of the entire file. You should also get access to more "dynamic" information like open namespaces (which could be influenced by a run_cmd), though it's less clear what that could look like

Last updated: Dec 20 2023 at 11:08 UTC