Topic: July meeting in Amsterdam
Rob Lewis (Jun 24 2019 at 08:47):
Hey everyone! We're planning to have a small Lean users meeting in Amsterdam next month, July 10-12. Sorry for the late notice, this has been planned sort of last minute. @Kevin Buzzard @Patrick Massot @Floris van Doorn will join the local crowd, and anyone else who wants to make the trip is more than welcome.
Rob Lewis (Jun 24 2019 at 08:48):
We'll start Wednesday afternoon to allow for travel time that morning.
Patrick Massot (Jul 04 2019 at 15:33):
Do we have a participant list for this Amsterdam meeting next week? It would help to prepare for greater efficiency. @Jan-David Salchow for instance, will you be around?
Jan-David Salchow (Jul 10 2019 at 05:37):
I’m still avoiding lean while finishing my thesis ;) But I’m happy to show up on Thursday or Friday evening
Jan-David Salchow (Jul 10 2019 at 05:38):
Is there a schedule for the meeting somewhere? Or is it purely informal?
Rob Lewis (Jul 10 2019 at 08:18):
Oops, sorry Patrick, I missed your message from before. Jan-David, there's no official schedule, but we can keep you updated!
Kevin Kappelmann (Jul 13 2019 at 11:15):
Hi, we had a brief discussion about tactics that people wish would be there. Here's the list
- Groebner basis: compute if something is an ideal
- Polya (
modules: normalforms like
continuity: Proving continuity of (composition of) functions
have : \exists ... with
rcases this ...
- fix the
- Label for
rcases label : term with ...
- some tactic to collect have statements, e.g. something like
have : ..., moreover have : ...., show ... by simp -- the last simp uses the last two collected hypotheses
Last updated: May 12 2021 at 04:19 UTC