~/bend-docscommunity

proofs/math/typed/float.bend checks

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

6 imports
import Base
import ../../../spec/math/generic.bend as SG
import ../../../src/math/generic.bend as G
import ../../../src/math/num.bend as N
import ../../../src/math/instances.bend as I
import ../../../src/math/f64.bend as F

Definitions

def pick_eq source · line 30 · raw

@-T:Data -> @+c:Bool -> @+a:T -> @+b:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pick(T, c, a, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.pick(T, c, a, b) : T}

def f32_ao source · line 153 · raw

@+a:F32 -> @+b:F32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.AddOver{a, b}) == False{} : Bool}

def f32_mo source · line 156 · raw

@+a:F32 -> @+b:F32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, b}) == False{} : Bool}

def f64_ao source · line 159 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.AddOver{a, b}) == False{} : Bool}

def f64_mo source · line 162 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, b}) == False{} : Bool}

def f32_min source · line 165 · raw

@+a:F32 -> @+b:F32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FMin.select(F32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is, a, b)

def f32_max source · line 168 · raw

@+a:F32 -> @+b:F32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FMax.select(F32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is, a, b)

def f32_clamp source · line 171 · raw

@+x:F32 -> @+lo:F32 -> @+hi:F32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FClamp.select(F32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is, x, lo, hi)

def f32_abs source · line 174 · raw

@+x:F32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FAbs.value(F32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is, x)

def f32_sign source · line 177 · raw

@+x:F32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FSign.select(F32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is, x)

def f32_sum source · line 180 · raw

@xs:List<&2, F32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FSum.fold(F32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is, xs)

def f32_prod source · line 183 · raw

@xs:List<&2, F32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FProd.fold(F32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is, xs)

def f32_pow source · line 186 · raw

@+x:F32 -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FPow.binary(F32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.f32_is, x, k)

def f64_min source · line 189 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FMin.select(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is, a, b)

def f64_max source · line 192 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FMax.select(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is, a, b)

def f64_clamp source · line 195 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FClamp.select(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is, x, lo, hi)

def f64_abs source · line 198 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FAbs.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is, x)

def f64_sign source · line 201 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FSign.select(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is, x)

def f64_sum source · line 204 · raw

@xs:List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FSum.fold(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is, xs)

def f64_prod source · line 207 · raw

@xs:List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FProd.fold(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is, xs)

def f64_pow source · line 210 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FPow.binary(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.f64_is, x, k)

Templates

template NoAddOver source · line 22 · raw

@-T:Data -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> Type

the instance never reports an overflow (floats round instead)

template NoMulOver source · line 25 · raw

@-T:Data -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> Type

template fmin_select source · line 37 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+a:T -> @+b:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FMin.select(T, op, test, a, b)

template fmax_select source · line 40 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+a:T -> @+b:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FMax.select(T, op, test, a, b)

template fclamp_c source · line 43 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> @+lo:T -> @+hi:T -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.clamp_ok(T, op, test, x, lo, hi, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.fclamp_pick(T, test, x, lo, hi, c) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, T>}

template fclamp_select source · line 52 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> @+lo:T -> @+hi:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FClamp.select(T, op, test, x, lo, hi)

template fabs_value source · line 55 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FAbs.value(T, op, test, x)

template sign_b source · line 58 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sign_below(T, op, test, x, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.pick(T, c, op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Neg{op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{})}), x) : T}

template sign_a source · line 65 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sign_above(T, op, test, x, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.pick(T, c, op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.pick(T, test(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{x, op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.ZeroOp{})}), op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Neg{op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{})}), x)) : T}

template fsign_select source · line 72 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FSign.select(T, op, test, x)

template sum_fold source · line 77 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-ao:NoAddOver(T, test) -> @xs:List<&2, T> -> @+acc:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sum_go(T, op, test, xs, Some{acc}) == Some{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.fold_add(T, op, xs, acc)} : Maybe<&2, T>}

template fsum_fold source · line 85 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-ao:NoAddOver(T, test) -> @xs:List<&2, T> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FSum.fold(T, op, test, xs)

template prod_fold source · line 89 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-mo:NoMulOver(T, test) -> @xs:List<&2, T> -> @+acc:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.prod_go(T, op, test, xs, Some{acc}) == Some{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.fold_mul(T, op, xs, acc)} : Maybe<&2, T>}

template fprod_fold source · line 97 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-mo:NoMulOver(T, test) -> @xs:List<&2, T> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FProd.fold(T, op, test, xs)

template binpow_zero source · line 104 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @fuel:Nat -> @+b:T -> @+a:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.binpow(T, op, fuel, 0n, b, a) == a : T}

k = 0 is a fixed point of the specification's loop

template sq_val_eq source · line 111 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @+c:Bool -> @+b:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sq_val(T, op, c, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.pick(T, c, op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Mul{b, b}), b) : T}

template sq_ok_eq source · line 118 · raw

@-T:Data -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-mo:NoMulOver(T, test) -> @+c:Bool -> @+b:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sq_ok(T, test, c, b, True{}) == True{} : Bool}

template mul_st_eq source · line 126 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-mo:NoMulOver(T, test) -> @+d:Bool -> @+b:T -> @+a:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.mul_st(T, op, test, d, b, True{}, (a, True{})) == (0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.pick(T, d, op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Mul{a, b}), a), True{}) : Pair(T, Bool)}

template pow_bin source · line 134 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-mo:NoMulOver(T, test) -> @+fuel:Nat -> @+k:Nat -> @+b:T -> @+a:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_go(T, op, test, fuel, k, b, True{}, (a, True{})) == Some{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.binpow(T, op, fuel, k, b, a)} : Maybe<&2, T>}

template fpow_binary source · line 147 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-mo:NoMulOver(T, test) -> @+x:T -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.FPow.binary(T, op, test, x, k)