mathlib documentation

core.init.data.unsigned.basic

def unsigned_sz :

Equations

unsigned_sz = 4294967295.succ

def unsigned :

Type

Equations

unsigned = fin unsigned_sz

def unsigned.of_nat' (n : ℕ) :

Equations

unsigned.of_nat' n = dite (n < unsigned_sz) (λ (h : n < unsigned_sz), ⟨n, h⟩) (λ (h : ¬n < unsigned_sz), ⟨0, zero_lt_unsigned_sz⟩)

def unsigned.to_nat (c : unsigned) :

Equations

c.to_nat = c.val

@[instance]

def unsigned.decidable_eq :

decidable_eq unsigned

Equations

unsigned.decidable_eq = have this : decidable_eq (fin unsigned_sz), from fin.decidable_eq unsigned_sz, this