~/bend-docscommunity

mathlib.bend checks

raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/mathlib.bend as Mathlib

8 imports
import Base
import ./bits.bend as Bits
import ./math.bend as Math
import ./num.bend as Nm
import ./rat.bend as Rt
import ./set.bend as Se
import ./series.bend as Sr
import ./mlib_linalg.bend as M2

Laws

law mlib_pop_7 provedsource · line 75 · raw

{mlib_pop(7) == 3 : U32}

law mlib_pow_3_5 provedsource · line 81 · raw

{mlib_pow(3, 5) == 243 : U32}

law mlib_gcd_12_8 provedsource · line 87 · raw

{mlib_gcd(12, 8) == 4 : U32}

law mlib_prime_7 provedsource · line 93 · raw

{mlib_is_prime(7) == True{} : Bool}

law mlib_modpow_345 provedsource · line 99 · raw

{mlib_mod_pow(3, 4, 5) == 1 : U32}

law mlib_trisum_10 provedsource · line 105 · raw

{mlib_trisum_u32(10n) == 55 : U32}

law mlib_radd_1_2_1_3_num provedsource · line 111 · raw

{mlib_radd_num(0x4c3090ea8722081700f9d99ea7503e43/rat.mk_rat(False{}, 1, 2), 0x4c3090ea8722081700f9d99ea7503e43/rat.mk_rat(False{}, 1, 3)) == 5 : U32}

law mlib_mat_det_example provedsource · line 117 · raw

{mlib_mat_det_u32(0x4c3090ea8722081700f9d99ea7503e43/mlib_linalg.mmat_example) == 10 : U32}

law mlib_set_size_two provedsource · line 123 · raw

{mlib_set_size(0x4c3090ea8722081700f9d99ea7503e43/set.sinsert(0x4c3090ea8722081700f9d99ea7503e43/set.sinsert(0x4c3090ea8722081700f9d99ea7503e43/set.sempty, 1), 2)) == 2 : U32}

law mlib_selftest_value provedsource · line 129 · raw

{mlib_selftest == 324 : U32}

Definitions

def mlib_pop source · line 30 · raw

@+x:U32 -> U32

def mlib_pow source · line 33 · raw

@+base:U32 -> @+exp:U32 -> U32

def mlib_gcd source · line 36 · raw

@+a:U32 -> @+b:U32 -> U32

def mlib_is_prime source · line 39 · raw

@+n:U32 -> Bool

def mlib_mod_pow source · line 42 · raw

@+base:U32 -> @+exp:U32 -> @+m:U32 -> U32

def mlib_trisum_u32 source · line 45 · raw

@n:Nat -> U32

def mlib_radd_num source · line 48 · raw

@a:0x4c3090ea8722081700f9d99ea7503e43/rat.Rat -> @b:0x4c3090ea8722081700f9d99ea7503e43/rat.Rat -> U32

def mlib_mat_det_u32 source · line 51 · raw

@m:0x4c3090ea8722081700f9d99ea7503e43/mlib_linalg.Mat2 -> U32

def mlib_set_size source · line 54 · raw

@s:0x4c3090ea8722081700f9d99ea7503e43/set.USet -> U32

def mlib_selftest source · line 61 · raw

U32