From 7eb6381f6844ca522883a2ccdd09564df8866b0e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Mar 2020 18:02:20 -0700 Subject: [PATCH] feat: throw error if unnecessary identifiers are provided --- src/Init/Lean/Elab/Tactic/Injection.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/Elab/Tactic/Injection.lean b/src/Init/Lean/Elab/Tactic/Injection.lean index 0ce5dc6419..15af6a8f6b 100644 --- a/src/Init/Lean/Elab/Tactic/Injection.lean +++ b/src/Init/Lean/Elab/Tactic/Injection.lean @@ -16,6 +16,10 @@ private def getInjectionNewIds (stx : Syntax) : List Name := if stx.isNone then [] else (stx.getArg 1).getArgs.toList.map Syntax.getId +private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Unit := +unless unusedIds.isEmpty $ + Meta.throwTacticEx `injection mvarId ("too many identifiers provided, unused: " ++ toString unusedIds) + @[builtinTactic «injection»] def evalInjection : Tactic := fun stx => do -- parser! nonReservedSymbol "injection " >> termParser >> withIds @@ -24,8 +28,8 @@ fun stx => do liftMetaTactic stx $ fun mvarId => do r ← Meta.injection mvarId fvarId ids (!ids.isEmpty); match r with - | Meta.InjectionResult.solved => pure [] - | Meta.InjectionResult.subgoal mvarId _ _ => pure [mvarId] + | Meta.InjectionResult.solved => do checkUnusedIds mvarId ids; pure [] + | Meta.InjectionResult.subgoal mvarId' _ unusedIds => do checkUnusedIds mvarId unusedIds; pure [mvarId'] end Tactic end Elab