English
Let SNum be the signed numeral system. There exists a natural map f: SNum → ℤ defined recursively by f(n) = -1 if the base indicator is true and 0 otherwise; and, if n is built from a flag a and a sub numeral k with IH = f(k), then f(n) = 2·IH + 1 if a is true and f(n) = 2·IH if a is false. This map assigns to each SNum its corresponding integer representation.
Русский
Пусть SNum — это система знаковых чисел. Существует естественное отображение f: SNum → ℤ, определяемое по рекурсии: f(n) = -1, если базовый флаг равен истине, и 0 в противном случае; если числитель состоит из флага a и части k с IH = f(k), тогда f(n) = 2·IH + 1, если a истинно, и f(n) = 2·IH, если a ложно. Это отображение присваивает каждому SNum его целочисленое представление.
LaTeX
$$$$\text{ofSnum}: \mathrm{SNum} \to \mathbb{Z}, \quad \text{ofSnum}(s) =
\begin{cases} -1, & \text{if base flag of } s \text{ is true}, \\ 0, & \text{otherwise}, \[4pt]
2 \cdot \text{ofSnum}(t) + 1, & \text{if } s \text{ extends with } a=\text{true}, \\ 2 \cdot \text{ofSnum}(t), & \text{if } s \text{ extends with } a=\text{false}. \end{cases}$$$$
Lean4
/-- Cast a `SNum` to the corresponding integer. -/
def ofSnum : SNum → ℤ :=
SNum.rec' (fun a => cond a (-1) 0) fun a _p IH => cond a (2 * IH + 1) (2 * IH)
