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

doc: clarify doc-string for Lean.Elab.Tactic.withLocation (#2909)

Browse source 
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).
This commit is contained in:
Scott Morrison 2023-11-20 14:29:32 +11:00 • committed by Sebastian Ullrich
parent 8881517018
commit 8b86beeb07
1 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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