mulExpr

Mathlib.Tactic.Linarith.Verification

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.mulExpr

Lean4

/-- `mulExpr n e` creates an `Expr` representing `n*e`.
When elaborated, the coefficient will be a native numeral of the same type as `e`.
-/
def mulExpr (n : ℕ) (e : Expr) : MetaM Expr := do
  let ⟨_, α, e⟩ ← inferTypeQ' e
  let inst : Q(Semiring $α) ← synthInstanceQ q(Semiring $α)
  return mulExpr' n inst e

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

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

Разделы

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

Аффилиация

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