spec/math/instances.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/spec/math/instances.bend as Instances

4 imports

import Base
import ../lib/common.bend as C
import ../../src/math/num.bend as N
import ../../src/math/natural.bend as M

Templates

template Ops.zero source · line 39 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-val:(@_:T -> Nat) -> Type

template Ops.one source · line 42 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-val:(@_:T -> Nat) -> Type

template Ops.add source · line 45 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @+a:T -> @+b:T -> @+h:{test(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.AddOver{a, b}) == False{} : Bool} -> Type

template Tests.add_over source · line 48 · raw

@-T:Data -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template Ops.sub source · line 51 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-val:(@_:T -> Nat) -> @+a:T -> @+b:T -> @+h:{Nat.is_le(val(b), val(a)) == True{} : Bool} -> Type

template Ops.mul source · line 54 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @+a:T -> @+b:T -> @+h:{test(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, b}) == False{} : Bool} -> Type

template Tests.mul_over source · line 57 · raw

@-T:Data -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template Ops.quot source · line 60 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-val:(@_:T -> Nat) -> @+a:T -> @+b:T -> @+h:{Nat.is_eq(val(b), 0n) == False{} : Bool} -> Type

template Ops.rem source · line 63 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-val:(@_:T -> Nat) -> @+a:T -> @+b:T -> @+h:{Nat.is_eq(val(b), 0n) == False{} : Bool} -> Type

template Ops.half source · line 66 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-val:(@_:T -> Nat) -> @+a:T -> Type

template Ops.mulmod source · line 69 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-val:(@_:T -> Nat) -> @+a:T -> @+b:T -> @+m:T -> @+ha:{Nat.is_lt(val(a), val(m)) == True{} : Bool} -> @+hb:{Nat.is_lt(val(b), val(m)) == True{} : Bool} -> Type

template Ops.pow2 source · line 72 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-val:(@_:T -> Nat) -> @+w:Nat -> @+k:Nat -> @+hk:{Nat.is_lt(k, w) == True{} : Bool} -> Type

template Ops.sqrt source · line 75 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-val:(@_:T -> Nat) -> @+a:T -> Type

template Ops.abs source · line 79 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @+a:T -> Type

unsigned: |a| is a

template Tests.lt source · line 82 · raw

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

template Tests.odd source · line 85 · raw

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

template Tests.is_zero source · line 88 · raw

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