const — Mathlib

English

There exists a constant-code function for Nat.Partrec outputs, giving a universal code for constant functions.

Русский

Существует константный код функции для Nat.Partrec, задающий универсальный код константной функции.

LaTeX

$$$\mathrm{Nat.Partrec.Code}.const : \mathbb{N} \to \mathrm{Code}$$$

Lean4

/-- Returns a code for the constant function outputting a particular natural. -/
protected def const : ℕ → Code
  | 0 => zero
  | n + 1 => comp succ (Code.const n)

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