toStained — Mathlib

Lean4
/-- `toStained stx` scans the input `Syntax` `stx` extracting identifiers and atoms, making an effort
to convert them to `Stained`.
The function is used to extract "location" information about `stx`: either explicit locations as in
`rw [] at locations` or implicit ones as `rw [h]`.

Whether or not what this function extracts really is a location will be determined by the linter
using data embedded in the `InfoTree`s. -/
partial def toStained : Syntax → Std.HashSet Stained
  | .node _ _ arg => (arg.map toStained).foldl (.union) { }
  | .ident _ _ val _ => {.name val}
  | .atom _ val =>
    match val with
    | "*" => {.wildcard}
    | "⊢" => {.goal}
    | "|" => {.goal}
    | _ => { }
  | _ => { }
Похожие утверждения