Zulip Chat Archive

Stream: general

Topic: list of filters


view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 05:19):

I've started a gist with two lists: a list of useful filters and a list of statements formulated with filters, then reformulated without filters. What do you think about including (an extended/improved version of) this list in some docs? @Patrick Massot @Sebastien Gouezel

view this post on Zulip Patrick Massot (Aug 14 2020 at 09:08):

The fist list uses the old notation for complement. I think both lists are useful, but the second one is a bit messy, and would be more useful if it included references to lemmas.

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 13:37):

Notation: fixed. The second one is messy, not "a bit" messy. Probably it should be organized into some sections (especially if expanded). The goal is to have some dictionary that people who never used filters can use to (a) understand mathlib theorems; (b) formulate their statements with filters.

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 14:02):

BTW, is there any (draft) text about filters for MIL?


Last updated: May 09 2021 at 19:11 UTC