English
Recursor for ENat using ⊤ and ↑a: given top-value constructor and a family of values indexed by ℕ, produce a function on ENat.
Русский
Рекурсор ENat, использующий ⊤ и ↑a: заданы верхняя константа и семейство значений, индексируемое ℕ, устанавливающее отображение на ENat.
LaTeX
$$$$ \\text{recTopCoe} : (C: ENat \\to \\mathrm{Sort}) \\to (C(\\top)) \\to (\\mathbb{N} \\to C(\\cdot)) \\to (\\mathbb{ENat}) \\; \\to \\mathrm{Sort} $$$$
Lean4
/-- Recursor for `ENat` using the preferred forms `⊤` and `↑a`. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
def recTopCoe {C : ℕ∞ → Sort*} (top : C ⊤) (coe : ∀ a : ℕ, C a) : ∀ n : ℕ∞, C n
| none => top
| Option.some a => coe a
