From 8b86beeb0780fcd7da85995f9a78933c0dffaa7b Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 20 Nov 2023 14:29:32 +1100 Subject: [PATCH] doc: clarify doc-string for Lean.Elab.Tactic.withLocation (#2909) In the previous doc-string, the sentence > "If any of the selected tactic applications fail, it will call `failed` with the main goal mvar." was false both for `Location.wildcard` (where it should have said "If all", not "If any") or for `Location.targets` (where `failed` is never called). --- src/Lean/Elab/Tactic/Location.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean index 6276f584ca..45c630920c 100644 --- a/src/Lean/Elab/Tactic/Location.lean +++ b/src/Lean/Elab/Tactic/Location.lean @@ -39,9 +39,16 @@ def expandOptLocation (stx : Syntax) : Location := open Meta -/-- Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given `loc`. -If any of the selected tactic applications fail, it will call `failed` with the main goal mvar. - -/ +/-- +Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given `loc`. + +* If `loc` is a list of locations, runs at each specified hypothesis (and finally the goal if `⊢` is included), + and fails if any of the tactic applications fail. +* If `loc` is `*`, runs at the target first and then the hypotheses in reverse order. + If all tactic applications fail, `withLocation` with call `failed` with the main goal mvar. + If the tactic application closes the main goal, `withLocation` will then fail with `no goals to be solved` + upon reaching the first hypothesis. +-/ def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget : TacticM Unit) (failed : MVarId → TacticM Unit) : TacticM Unit := do match loc with | Location.targets hyps type =>