From 9f49dfd0e8ea1df4c92bfae027439b57ac080d3a Mon Sep 17 00:00:00 2001
From: FR <zhao.yu-yang@foxmail.com>
Date: Mon, 3 Jun 2024 16:27:04 +0800
Subject: [PATCH] chore: remove `binder_predicate`

It has been upstreamed to Lean4.
---
 Batteries/Util/ExtendedBinder.lean | 19 -------------------
 1 file changed, 19 deletions(-)

diff --git a/Batteries/Util/ExtendedBinder.lean b/Batteries/Util/ExtendedBinder.lean
index 33629b7cc0..d577e1d785 100644
--- a/Batteries/Util/ExtendedBinder.lean
+++ b/Batteries/Util/ExtendedBinder.lean
@@ -52,22 +52,3 @@ macro_rules -- TODO: merging the two macro_rules breaks expansion
   | `(∀ᵉ _ : $ty:term, $b) => `(∀ _ : $ty:term, $b)
   | `(∀ᵉ $x:ident : $ty:term, $b) => `(∀ $x:ident : $ty:term, $b)
   | `(∀ᵉ $x:binderIdent $p:binderPred, $b) => `(∀ $x:binderIdent $p:binderPred, $b)
-
-open Parser.Command in
-/--
-Declares a binder predicate.  For example:
-```
-binder_predicate x " > " y:term => `($x > $y)
-```
--/
-syntax (name := binderPredicate) (docComment)? (Parser.Term.attributes)? (attrKind)?
-  "binder_predicate" optNamedName optNamedPrio ppSpace ident (ppSpace macroArg)* " => "
-    term : command
-
-open Linter.MissingDocs Parser Term in
-/-- Missing docs handler for `binder_predicate` -/
-@[missing_docs_handler binderPredicate]
-def checkBinderPredicate : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
-    if stx[4].isNone then lint stx[3] "binder predicate"
-    else lintNamed stx[4][0][3] "binder predicate"