mapStringsM

Mathlib.Util.Superscript

URI: https://scilib.ai/kg/mathlib#Std.Format.mapStringsM

Lean4

/-- Map over the strings in a `Format`. -/
def _root_.Std.Format.mapStringsM {m} [Monad m] (f : Format) (f' : String → m String) : m Format :=
  match f with
  | .group f b => (.group · b) <$> Std.Format.mapStringsM f f'
  | .tag t g => .tag t <$> Std.Format.mapStringsM g f'
  | .append f g => .append <$> Std.Format.mapStringsM f f' <*> Std.Format.mapStringsM g f'
  | .nest n f => .nest n <$> Std.Format.mapStringsM f f'
  | .text s => .text <$> f' s
  | .align _ | .line | .nil => pure f

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

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

Разделы

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

Аффилиация

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