capSourceInfo

Mathlib.Tactic.Linter.PPRoundtrip

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.capSourceInfo

Lean4

/-- `capSourceInfo s p` "shortens" all end-position information in the `SourceInfo` `s` to be
at most `p`, trimming down also the relevant substrings. -/
def capSourceInfo (s : SourceInfo) (p : Nat) : SourceInfo :=
  match s with
  | .original leading pos trailing endPos =>
    .original leading pos { trailing with stopPos := ⟨min endPos.1 p⟩ } ⟨min endPos.1 p⟩
  | .synthetic pos endPos canonical => .synthetic pos ⟨min endPos.1 p⟩ canonical
  | .none => s

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru