~/bend-docscommunity

proofs/math/typed/examples.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/examples.bend as Examples

4 imports
import Base
import ../../../spec/math/generic.bend as SG
import ../../../spec/math/instances.bend as SI
import ../../../src/math/instances.bend as I

Definitions

def gcd source · line 15 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Gcd.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 12, 18)

def gcd_zero source · line 18 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Gcd.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0, 7)

def lcm source · line 21 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Lcm.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 4, 6)

def lcm_zero source · line 24 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Lcm.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 0, 6)

def gcd_all source · line 27 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.GcdAll.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, [12, 18, 8])

def gcd_all_empty source · line 30 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.GcdAll.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, [])

def lcm_all source · line 33 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.LcmAll.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, [2, 3, 4])

def lcm_all_zero source · line 36 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.LcmAll.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, [2, 0, 3])

def iroot source · line 39 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Iroot.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 27, 3n)

def iroot_zero_degree source · line 42 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Iroot.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 27, 0n)

def ilog source · line 45 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Ilog.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 100, 10)

def ilog_zero source · line 48 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Ilog.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0, 10)

def ilog_base_one source · line 51 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Ilog.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 100, 1)

def factorial source · line 54 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Factorial.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 5)

def factorial_zero source · line 57 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Factorial.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 0)

def perm source · line 60 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Perm.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 5, 2)

def perm_over source · line 63 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Perm.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 2, 5)

def comb source · line 66 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Comb.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 6, 3)

def comb_over source · line 69 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Comb.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 3, 6)

def pow_mod source · line 72 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.PowMod.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 3, 4, 5)

def pow_mod_zero_modulus source · line 75 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.PowMod.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 3, 4, 0)

def mod_inverse source · line 78 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.ModInverse.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 3, 7)

def mod_inverse_not_coprime source · line 81 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.ModInverse.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 2, 4)

def mod_inverse_zero_modulus source · line 84 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.ModInverse.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 3, 0)

def divmod source · line 87 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.DivMod.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 17, 5)

def divmod_zero source · line 90 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.DivMod.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 17, 0)

def bit_length source · line 93 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.BitLength.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 255)

def bit_length_zero source · line 96 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.BitLength.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0)

def clamp source · line 99 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Clamp.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 5, 1, 3)

def clamp_domain source · line 102 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Clamp.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 5, 3, 1)

def min source · line 105 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Min.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 2, 5)

def min_tie source · line 108 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Min.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 3, 3)

def max source · line 111 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Max.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 2, 5)

def abs source · line 114 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Abs.identity(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 7)

def sign source · line 117 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Sign.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 9)

def sign_zero source · line 120 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Sign.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0)

def sum source · line 123 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Sum.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, [1, 2, 3])

def prod source · line 126 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Prod.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, [2, 3, 0])

def pow source · line 129 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Pow.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 3, 4n)

def pow_zero source · line 132 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Pow.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 0, 0n)

def op_zero source · line 137 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.zero(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val)

def op_one source · line 140 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.one(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val)

def op_add source · line 143 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.add(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 7, 9, {==})

def test_add_over source · line 146 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.add_over(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 32n, 7, 9)

def op_sub source · line 149 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.sub(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 9, 7, {==})

def op_mul source · line 152 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.mul(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 7, 9, {==})

def test_mul_over source · line 155 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.mul_over(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 32n, 7, 9)

def op_quot source · line 158 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.quot(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 17, 5, {==})

def op_rem source · line 161 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.rem(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 17, 5, {==})

def op_half source · line 164 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.half(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 17)

def op_mulmod source · line 167 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.mulmod(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 5, 6, 7, {==}, {==})

def op_pow2 source · line 170 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.pow2(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 32n, 5n, {==})

def op_abs source · line 173 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.abs(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 7)

def test_lt source · line 176 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.lt(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 3, 5)

def test_odd source · line 179 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.odd(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 7)

def test_is_zero source · line 182 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.is_zero(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0)