capSyntax — Mathlib

Lean4
/-- `capSyntax stx p` applies `capSourceInfo · s` to all `SourceInfo`s in all
`node`s, `atom`s and `ident`s contained in `stx`.

This is used to trim away all "fluff" that follows a command: comments and whitespace after
a command get removed with `capSyntax stx stx.getTailPos?.get!`.
-/
partial def capSyntax (stx : Syntax) (p : Nat) : Syntax :=
  match stx with
  | .node si k args => .node (capSourceInfo si p) k (args.map (capSyntax · p))
  | .atom si val => .atom (capSourceInfo si p) (val.take p)
  | .ident si r v pr => .ident (capSourceInfo si p) { r with stopPos := ⟨min r.stopPos.1 p⟩ } v pr
  | s => s
Похожие утверждения