natSize — Mathlib

English

The number of bits required to represent a Num, defined by: 0 maps to 0, and pos n uses PosNum.natSize n.

Русский

Число бит, необходимое для представления Num, задано: 0 → 0, a pos n → PosNum.natSize n.

LaTeX

$$def natSize : Num → Nat | 0 => 0 | pos n => PosNum.natSize n$$

Lean4

/-- The number of bits required to represent a `Num`, as a `Nat`. `size 0` is defined to be `0`. -/
def natSize : Num → Nat
  | 0 => 0
  | pos n => PosNum.natSize n

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