Zulip Chat Archive
Stream: Lean Together 2019
Topic: Questions about Lean 4
Joseph Corneli (Jan 07 2019 at 14:29):
"any chance of the tool you're presenting will allow us to reimplement parameters?"
Joseph Corneli (Jan 07 2019 at 14:29):
"I was hoping parameters would get sane... now I have more tactics to write"
Joseph Corneli (Jan 07 2019 at 14:29):
... I think we can make something better than parameters. Reinterpret them.
Joseph Corneli (Jan 07 2019 at 14:30):
"Type reflection... what's going to happen? Will we have type of expressions of a give type?"
Joseph Corneli (Jan 07 2019 at 14:30):
... Leo in Lean, past, present and future talks about this.
Joseph Corneli (Jan 07 2019 at 14:30):
"If you go back to 'how to port' - changes in the meta-interface. We have some tactics in mathlib for example. They need to be rewritten because the expression syntax changes?"
Joseph Corneli (Jan 07 2019 at 14:31):
"Something like local_const?"
... that's just a search and replace
Joseph Corneli (Jan 07 2019 at 14:31):
"Primitive projections..."
Joseph Corneli (Jan 07 2019 at 14:32):
"Sugared version of let... let goes down into the kernel"
... you can come up with your own syntax, and now say let is just syntax for..."
Joseph Corneli (Jan 07 2019 at 14:33):
... there are no foundational changes, except for primitive projection and mutual induction. projection is more of an implementation detail.
... Lean 5??? Lean 4 is as general as we can make it. There will not be a Lean 5 in the near future.
"Lean 3 has failed? What's the definition of failure?"
... Getting issues at Github that you can't implement with the current system and getting frustrated with that.
"So, people asking Leo to make syntax changes..."
Joseph Corneli (Jan 07 2019 at 14:35):
"Instead of waiting for completion of the project, could we use the new parser ...?"
... You can't use it without the macro expander.
"But if we wanted to have a beautiful HTML file... or a linter for code?"
... But you may still want information from the elaborator. You'll need more information from just the syntax tree?
Joseph Corneli (Jan 07 2019 at 14:35):
"We have a trend to move to cubical type checkers...?"
... no foundational changes in the logic.
"It is possible to embed cubical type theory... We can construct the syntax. "
... Embed things like Lean 3 HoTT did.
Joseph Corneli (Jan 07 2019 at 14:36):
"There are some issues with the way coersions work..."
... we're not yet sure how they should work ideally.
Sebastian Ullrich (Jan 07 2019 at 15:44):
"Instead of waiting for completion of the project, could we use the new parser ...?"
... You can't use it without the macro expander.
To expand (heh) on that, Lean's extensible syntax (in both Lean 3 and 4) means that you can't just throw the parser at an arbitrary Lean file. You first have to register all notations from the imports, then handle notations in the file, including scoping local notations to enclosing sections, etc...
Koundinya Vajjha (Jan 07 2019 at 16:11):
No one asked the million dollar question? When is it coming out? :grinning_face_with_smiling_eyes:
Johan Commelin (Jan 07 2019 at 16:11):
201X seems to be the default answer...
Joseph Corneli (Jan 07 2019 at 16:15):
So presumably later this year, see title of thread.
Joseph Corneli (Jan 07 2019 at 16:15):
er, title of Stream, rather
Kevin Buzzard (Jan 07 2019 at 19:04):
I asked this directly to Sebastian and he said that 201X was not supposed to imply before 2020 -- it was just an unfortunate choice of notation.
Simon Hudon (Jan 07 2019 at 21:38):
@Kevin Buzzard That's a fair point. Before it's release, C++ 2011 was known as C++0x
Last updated: Dec 20 2023 at 11:08 UTC