Commit 2021-12-01 14:43 e4efce37

feat: { x + 10 | x < 10 } (#118) Ports the set replacement syntax from Lean 3. For that, I've also added a general framework where you can register relations to use in binders (e.g. ∀ ε > 0, ∃ x ∈ ball y ε, ...). You can register a new relation with a single command, and it automatically works in quantifiers, set comprehensions, etc.:

local binder_predicate x " within " eps:term " of " y:term => `(dist $x $y <= $eps)
-- ∃ x within ε of y, ...
-- { x within ε of y | ... }

The quantified variable can only be at the beginning, because this makes parsing much easier. (So no ∀ 42 < x < 99, x < 300.) There is also no unexpander support yet. See also https://github.com/leanprover-community/mathport/issues/13. Mario suggested also supporting ∀ ε δ > 0, ... there, but I'm not sure how important that is.