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

feat: throw error if unnecessary identifiers are provided

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-08 18:02:20 -07:00
parent d24acdde46
commit 7eb6381f68
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Lean/Elab/Tactic/Injection.lean
View file

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