July meeting in Amsterdam

Stream: general

[Rob Lewis]

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]

We'll start Wednesday afternoon to allow for travel time that morning.

[Patrick Massot]

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]

I’m still avoiding lean while finishing my thesis ;) But I’m happy to show up on Thursday or Friday evening

[Jan-David Salchow]

Is there a schedule for the meeting somewhere? Or is it purely informal?

[Rob Lewis]

Oops, sorry Patrick, I missed your message from before. Jan-David, there's no official schedule, but we can keep you updated!

[Kevin Kappelmann]

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 (nonlinarith and field)
- modules: normalforms like ring, abel
- continuity: Proving continuity of (composition of) functions
- obtain: combine have : \exists ... with rcases this ...
- fix the WLOG tactic
- Label for rcases: 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