English
ofNat' provides a canonical embedding of natural numbers into Num via binary representation, defined by a binary recursion.
Русский
ofNat' задаёт каноническое вложение натуральных чисел в Num через двоичное представление, задаваемое рекурсией по битам.
LaTeX
$$$\\operatorname{ofNat'} : \\mathbb N \\to \\operatorname{Num} \\\\ \\operatorname{ofNat'}(n) = \\operatorname{Nat.binaryRec} 0 (\\lambda b \\_ , \\text{cond } b \\operatorname{Num.bit1} \\operatorname{Num.bit0})\\, n$$$
Lean4
/-- Converts a `Nat` to a `Num`. -/
def ofNat' : ℕ → Num :=
Nat.binaryRec 0 (fun b _ => cond b Num.bit1 Num.bit0)
