From 03524305dbf3bef40ba603e9ef5ef474022c45e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 May 2022 07:22:30 -0700 Subject: [PATCH] fix: `findTag?` If there is an exact match, return it. --- src/Lean/Elab/Tactic/BuiltinTactic.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index fdbf41a5e9..abf1516fe0 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -258,13 +258,16 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : | _ => throwUnsupportedSyntax /-- - First method searches for a metavariable `g` s.t. `tag` is a suffix of its name. - If none is found, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/ + Searches for a metavariable `g` s.t. `tag` is its exact name. + If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name. + If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/ private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do - let mvarId? ← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← getMVarDecl mvarId).userName - match mvarId? with + match (← mvarIds.findM? fun mvarId => return tag == (← getMVarDecl mvarId).userName) with | some mvarId => return mvarId - | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← getMVarDecl mvarId).userName + | none => + match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← getMVarDecl mvarId).userName) with + | some mvarId => return mvarId + | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← getMVarDecl mvarId).userName def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId := do if hs.isEmpty then