Topic: list of filters
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
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.
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.
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