mkMapping

Mathlib.Util.Superscript

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Superscript.mkMapping

Lean4

/-- Constructs a mapping (intended for compile time use). Panics on violated invariants. -/
def mkMapping (s₁ s₂ : String) : Mapping :=
  Id.run
    (do
      let mut toNormal := { }
      let mut toSpecial := { }
      assert! s₁.length == s₂.length
      for sp in s₁.toSubstring, nm in s₂ do
        assert! !toNormal.contains sp
        assert! !toSpecial.contains nm
        toNormal := toNormal.insert sp nm
        toSpecial := toSpecial.insert nm sp
      pure { toNormal, toSpecial })

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

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

Разделы

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

Аффилиация

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