getUnlintedRanges — Mathlib

Lean4
/-- Given an array `a` of `SyntaxNodeKind`s, we accumulate the ranges of the syntax nodes of the
input syntax whose kind is in `a`.

The linter uses this information to avoid emitting a warning for nodes with kind contained in
`unlintedNodes`.
-/
def getUnlintedRanges (a : Array SyntaxNodeKind) : Std.HashSet String.Range → Syntax → Std.HashSet String.Range
  | curr, s@(.node _ kind args) =>
    let new := args.foldl (init := curr) (·.union <| getUnlintedRanges a curr ·)
    if a.contains kind then new.insert (s.getRange?.getD default) else new
  | curr, .atom info "where" => if let some trail := info.getRangeWithTrailing? then curr.insert trail else curr
  | curr, _ => curr
Похожие утверждения