spec/math/fixed.bend checks

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

4 imports

import Base
import ../lib/common.bend as C
import ../../src/math/fixed.bend as F
import ./number.bend as SN

Definitions

def keep source · line 48 · raw

@ok:Bool -> @+n:Nat -> Maybe<&2, Nat>

def cnat source · line 56 · raw

@+w:Nat -> @+n:Nat -> Maybe<&2, Nat>

n when it fits w bits

def ov_flag source · line 64 · raw

@-T:Data -> @r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T> -> Bool

def bn source · line 69 · raw

@b:Bool -> Nat

def saturated source · line 77 · raw

@+w:Nat -> @+n:Nat -> @+r:Nat -> @ok:Bool -> Bool

r is n when n fits w bits, and the largest w-bit value otherwise

def IsPrime.value source · line 187 · raw

@+a:U32 -> Type

def no_prime source · line 191 · raw

@k:Nat -> @+lo:Nat -> Bool

no prime m with lo <= m < lo + k

def NextPrime.found source · line 199 · raw

@+n:U32 -> @+p:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_next_prime(n) == Some{p} : Maybe<&2, U32>} -> Type

a found p is a prime above n, and none lies strictly between them

def NextPrime.none source · line 203 · raw

@+n:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_next_prime(n) == None{} : Maybe<&2, U32>} -> @+m:Nat -> @+hm:{Nat.is_lt(U32.to_nat(n), m) == True{} : Bool} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, m) == True{} : Bool} -> Type

None: no prime m with n < m < 2^32

def nats source · line 208 · raw

@xs:List<&2, U32> -> List<&2, Nat>

def le_digits source · line 216 · raw

@k:Nat -> @+n:Nat -> List<&2, Nat>

the k lowest base-256 digits of n, least significant first

def digit_on source · line 231 · raw

@r:Maybe<&2, Nat> -> @ok:Bool -> @+x:Nat -> Maybe<&2, Nat>

the value of exactly k base-256 digits, least significant first; None for another length or a digit of 256 or more

def from_le source · line 242 · raw

@k:Nat -> @xs:List<&2, Nat> -> Maybe<&2, Nat>

Templates

template mval source · line 41 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @r:Maybe<&2, T> -> Maybe<&2, Nat>

template ov_val source · line 59 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T> -> Nat

template CheckedAdd.value source · line 86 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> Maybe<&2, T>) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template CheckedSub.value source · line 89 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> Maybe<&2, T>) -> @+a:T -> @+b:T -> Type

template CheckedMul.value source · line 92 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> Maybe<&2, T>) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template CheckedDiv.value source · line 95 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> Maybe<&2, T>) -> @+a:T -> @+b:T -> Type

template CheckedRem.value source · line 98 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> Maybe<&2, T>) -> @+a:T -> @+b:T -> Type

template CheckedPow.value source · line 101 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> Maybe<&2, T>) -> @+w:Nat -> @+a:T -> @+e:U32 -> Type

template CheckedShl.value source · line 104 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> Maybe<&2, T>) -> @+w:Nat -> @+a:T -> @+s:U32 -> Type

template CheckedShr.value source · line 107 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> Maybe<&2, T>) -> @+w:Nat -> @+a:T -> @+s:U32 -> Type

template WrappingAdd.value source · line 112 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> T) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template WrappingSub.value source · line 115 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> T) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template WrappingMul.value source · line 118 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> T) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template WrappingPow.value source · line 121 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> T) -> @+w:Nat -> @+a:T -> @+e:U32 -> Type

template WrappingShl.value source · line 124 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> T) -> @+w:Nat -> @+a:T -> @+s:U32 -> Type

template WrappingShr.value source · line 127 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> T) -> @+w:Nat -> @+a:T -> @+s:U32 -> Type

template SaturatingAdd.value source · line 132 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> T) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template SaturatingSub.value source · line 135 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> T) -> @+a:T -> @+b:T -> Type

template SaturatingMul.value source · line 138 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> T) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template SaturatingPow.value source · line 141 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> T) -> @+w:Nat -> @+a:T -> @+e:U32 -> Type

template OverflowingAdd.value source · line 146 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template OverflowingAdd.flag source · line 149 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template OverflowingSub.value source · line 152 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template OverflowingSub.flag source · line 155 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+a:T -> @+b:T -> Type

template OverflowingMul.value source · line 158 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template OverflowingMul.flag source · line 161 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:T -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template OverflowingPow.value source · line 164 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+w:Nat -> @+a:T -> @+e:U32 -> Type

template OverflowingPow.flag source · line 167 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+w:Nat -> @+a:T -> @+e:U32 -> Type

template OverflowingShl.value source · line 170 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+w:Nat -> @+a:T -> @+s:U32 -> Type

template OverflowingShl.flag source · line 173 · raw

@-T:Data -> @-f:(@+x:T -> @+y:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+a:T -> @+s:U32 -> @+w:Nat -> Type

template OverflowingShr.value source · line 176 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> @+y:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+w:Nat -> @+a:T -> @+s:U32 -> Type

template OverflowingShr.flag source · line 179 · raw

@-T:Data -> @-f:(@+x:T -> @+y:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.Over<T>) -> @+a:T -> @+s:U32 -> @+w:Nat -> Type

template BitCount.value source · line 184 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> Nat) -> @+w:Nat -> @+a:T -> Type

template ToBytes.le source · line 223 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> List<&2, U32>) -> @+nb:Nat -> @+a:T -> Type

template ToBytes.be source · line 226 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@+x:T -> List<&2, U32>) -> @+nb:Nat -> @+a:T -> Type

template FromBytes.le source · line 251 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@_:List<&2, U32> -> Maybe<&2, T>) -> @+nb:Nat -> @bs:List<&2, U32> -> Type

template FromBytes.be source · line 254 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @-f:(@_:List<&2, U32> -> Maybe<&2, T>) -> @+nb:Nat -> @bs:List<&2, U32> -> Type