Commit 2020-08-17 12:15 1a8f6bf9
View on Github →feat(lint): improved ge_or_gt linter (#3810)
The linter will now correctly accepts occurrences of f (≥) and ∃ x ≥ t, b
The linter will still raise a false positive on ∃ x y ≥ t, b (with 2+ bound variables in a single binder that involves >/≥)
In contrast to the previous version of the linter, this one does check hypotheses.
This should reduce the @[nolint ge_or_gt] attributes from ~160 to ~10.