mkTerm

Mathlib.Tactic.Abel

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Abel.mkTerm

Lean4

/-- Evaluate a term with coefficient `n`, atom `x` and successor terms `a`. -/
def mkTerm (n x a : Expr) : M Expr :=
  iapp ``term #[n, x, a]

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

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

Разделы

Аффилиация

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