repr' — Mathlib

English

A printer repr' is defined that assigns to each natural precision a formatted representation of ONote objects.

Русский

Определена функция печати repr', которая задаёт для каждого натурального уровня точности форматированное отображение объектов ONote.

LaTeX

$$$\mathrm{repr'} : \mathbb{N} \to \mathrm{ONote} \to \mathrm{Format}$$$

Lean4

/-- Print an ordinal notation -/
def repr' (prec : ℕ) : ONote → Format
  | zero => "0"
  | oadd e n a =>
    Repr.addAppParen ("oadd " ++ (repr' max_prec e) ++ " " ++ Nat.repr (n : ℕ) ++ " " ++ (repr' max_prec a)) prec

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