feat: add support for not-equals in exists (#384)

leanprover-community · Nov 25, 2023 · a652e09 · a652e09
1 parent 3044327
commit a652e09
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Std/Util/ExtendedBinder.lean b/Std/Util/ExtendedBinder.lean
@@ -136,3 +136,5 @@ 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)