deindentString

Mathlib.Tactic.Linter.DocString

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

Lean4

/-- Currently, this function simply removes `currIndent` spaces after each `\n`
in the input string `docString`.

If/when the `docString` linter expands, it may take on more string processing.
-/
def deindentString (currIndent : Nat) (docString : String) : String :=
  let indent : String := ⟨'\n' :: List.replicate currIndent ' '⟩
  docString.replace indent " "

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

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

Разделы

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

Аффилиация

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