Zulip Chat Archive

Stream: Lean Together 2021

Topic: Thursday schedule

Rob Lewis (Jan 07 2021 at 07:19):

Because we're all eager to hear more details about Lean 4, Leo agreed to continue with the metaprogramming slides we ran out of time for yesterday. We'll add this to the schedule at the end of today's session, at . This talk will be technical: if you don't care about metaprogramming, you're welcome to start the social time as scheduled, and the rest of us will join you a bit later.

Rob Lewis (Jan 07 2021 at 17:05):

We're running 10 minutes behind. We'll resume shortly after

Last updated: Dec 20 2023 at 11:08 UTC