From 487bcaaf2b1e81608b4a00bee78bf0d96bc993ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 6 Apr 2021 19:11:59 -0700 Subject: [PATCH] chore: remove dead coe --- src/Init/Prelude.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 77c7521e17..9e4da15fd0 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1729,12 +1729,6 @@ def isMissing : Syntax → Bool def isNodeOf (stx : Syntax) (k : SyntaxNodeKind) (n : Nat) : Bool := and (stx.isOfKind k) (beq stx.getNumArgs n) -/-- - We use this function to implement `Syntax` pattern matching. - We can use it to tweak the behavior of the matcher for special node such as `Syntax.missing`. -/ -def isNodeOf' (stx : Syntax) (k : SyntaxNodeKind) (n : Nat) : Bool := - stx.isNodeOf k n - def isIdent : Syntax → Bool | ident _ _ _ _ => true | _ => false