get

Mathlib.Data.QPF.Multivariate.Constructions.Const

URI: https://scilib.ai/kg/mathlib#MvQPF.Const.get

English

The destructor for the constant functor returns the underlying value of type A.

Русский

Деструктор константного функторa возвращает лежащие в константе значения типа A.

LaTeX

$$$\mathrm{Const.get}(z) = a \quad\text{for } z \in \mathrm{Const}\; n\; A\; \alpha\text{ with } z=\mathrm{Const.mk}(a).$$$

Lean4

/-- Destructor for constant functor -/
protected def get (x : Const n A α) : A :=
  x

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

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

Разделы

Аффилиация

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