addSynonym

Mathlib.Tactic.Explode.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Explode.Entries.addSynonym

Lean4

/-- Add a pre-existing entry to the `ExprMap` for an additional expression.
This is used by `let` bindings where `expr` is an fvar. -/
def addSynonym (entries : Entries) (expr : Expr) (entry : Entry) : Entries :=
  ⟨entries.s.insert expr entry, entries.l⟩

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

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

Разделы

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

Аффилиация

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