Stream: Lean Together 2021
Topic: porting mathlib to Lean 4
Rob Lewis (Jan 05 2021 at 09:30):
On yesterday's schedule we had a time slot to discuss porting mathlib to Lean 4. We very happily yielded this time to Leo and Sebastian's Lean 4 presentation -- to discuss porting, we need as much information as we can get about the target of the port!
Rob Lewis (Jan 05 2021 at 09:31):
Our social time immediately crashed Wonder, so we reconvened on Zoom, and there was an impromptu porting discussion there.
Rob Lewis (Jan 05 2021 at 09:32):
This wasn't a guided discussion and certainly no plans or decisions were made, so don't feel that you missed out on anything juicy if you weren't there :)
Rob Lewis (Jan 05 2021 at 09:33):
We won't have time to reschedule a porting discussion during this workshop, but we'll come back to the idea after people have had some time to play around with the brand new Lean 4 release. Stay tuned.
Last updated: May 08 2021 at 22:13 UTC