mathlib documentation

core.init.data.unsigned.ops

def unsigned.of_nat (n : ℕ) :

Equations

unsigned.of_nat n = fin.of_nat n

@[instance]

def unsigned.has_zero :

has_zero unsigned

Equations

unsigned.has_zero = {zero := fin.of_nat 0}

@[instance]

def unsigned.has_one :

has_one unsigned

Equations

unsigned.has_one = {one := fin.of_nat 1}

@[instance]

def unsigned.has_add :

has_add unsigned

Equations

unsigned.has_add = {add := fin.add unsigned_sz}

@[instance]

def unsigned.has_sub :

has_sub unsigned

Equations

unsigned.has_sub = {sub := fin.sub unsigned_sz}

@[instance]

def unsigned.has_mul :

has_mul unsigned

Equations

unsigned.has_mul = {mul := fin.mul unsigned_sz}

@[instance]

def unsigned.has_mod :

has_mod unsigned

Equations

unsigned.has_mod = {mod := fin.mod unsigned_sz}

@[instance]

def unsigned.has_div :

has_div unsigned

Equations

unsigned.has_div = {div := fin.div unsigned_sz}

@[instance]

def unsigned.has_lt :

has_lt unsigned

Equations

unsigned.has_lt = {lt := fin.lt unsigned_sz}

@[instance]

def unsigned.has_le :

has_le unsigned

Equations

unsigned.has_le = {le := fin.le unsigned_sz}