max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: findTag?

Browse source 
If there is an exact match, return it.
This commit is contained in:
Leonardo de Moura 2022-05-01 07:22:30 -07:00
parent a0678b5f6f
commit 03524305db
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Elab/Tactic/BuiltinTactic.lean
View file

@ -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