zoomString

Mathlib.Tactic.Linter.PPRoundtrip

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

Lean4

/-- `zoomString str centre offset` returns the substring of `str` consisting of the `offset`
characters around the `centre`th character. -/
def zoomString (str : String) (centre offset : Nat) : Substring :=
  { str := str, startPos := ⟨centre - offset⟩, stopPos := ⟨centre + offset⟩ }

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

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

Разделы

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

Аффилиация

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