Revert "feat: add support for not-in in exists (#425)" (#427)

This `binder_predicate` is already defined in another file, and so this causes ambiguity in the grammar.
leanprover-community · Dec 8, 2023 · b197bd2 · b197bd2
1 parent 63c387d
commit b197bd2
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/Std/Util/ExtendedBinder.lean b/Std/Util/ExtendedBinder.lean
@@ -138,5 +138,3 @@ binder_predicate x " < " y:term => `($x < $y)
 binder_predicate x " ≤ " y:term => `($x ≤ $y)
 /-- Declare `∃ x ≠ y, ...` as syntax for `∃ x, x ≠ y ∧ ...` -/
 binder_predicate x " ≠ " y:term => `($x ≠ $y)
-/-- Declare `∃ x ∉ y, ...` as syntax for `∃ x, x ∉ y ∧ ...` -/
-binder_predicate x " ∉ " y:term => `($x ∉ $y)