Zulip Chat Archive

Stream: Lean Together 2019

Topic: Questions about Lean 4


view this post on Zulip Joseph Corneli (Jan 07 2019 at 14:29):

"any chance of the tool you're presenting will allow us to reimplement parameters?"

view this post on Zulip Joseph Corneli (Jan 07 2019 at 14:29):

"I was hoping parameters would get sane... now I have more tactics to write"

view this post on Zulip Joseph Corneli (Jan 07 2019 at 14:29):

... I think we can make something better than parameters. Reinterpret them.

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

view this post on Zulip Joseph Corneli (Jan 07 2019 at 14:30):

... Leo in Lean, past, present and future talks about this.

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

view this post on Zulip Joseph Corneli (Jan 07 2019 at 14:31):

"Something like local_const?"
... that's just a search and replace

view this post on Zulip Joseph Corneli (Jan 07 2019 at 14:31):

"Primitive projections..."

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

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Jan 07 2019 at 16:11):

201X seems to be the default answer...

view this post on Zulip Joseph Corneli (Jan 07 2019 at 16:15):

So presumably later this year, see title of thread.

view this post on Zulip Joseph Corneli (Jan 07 2019 at 16:15):

er, title of Stream, rather

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

view this post on Zulip 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: May 08 2021 at 22:13 UTC