## Stream: general

### 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 (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

Last updated: May 12 2021 at 04:19 UTC