bend-lawful-stdlib

Search uses release 0.1.0.0 · 248 definitions

Releases (1)

type Val
type Formatp: mantissa bits; emin, emax: lowest and highest exponent (offset by 300) of a mantissa's last bit
def binary32binary32: 24 bits; smallest subnormal 2^-149; largest 2^104 * (2^24 - 1)
def stripthe same value with its low zero bits moved into the exponent and its high zero bits dropped, so that equal values are equal terms
def canon
def over.go
def over
def round.up
def round.fin
def round.go
def roundthe float of format f nearest to (-1)^neg * m * 2^(e - 300), ties to even
def add.fin.cmpadd two finite values once their mantissas share the exponent e
def add.fin.signs
def add.fin.aligned
def add.fin.go
def add.fin
def add.inf.go
def add.inf
def add.zero
def spec_addIEEE addition: the exact sum, rounded; x + (-x) is +0
def neg
def spec_sub
def mul.fin
def mul.inf
def mul.zero
def spec_mulIEEE multiplication: the exact product, rounded

def bits
def of_bits
def decode.go
def decode.cls
def decode.sign
def decode.exp
def decode.man
def decodethe exact value of a float
def signthe sign bit, as it sits above the 8 exponent bits
def worda word from its fields: 23 mantissa bits, then exponent and sign above
def first
def alignm moved to have its last bit at exponent t
def field
def put
def encode.fina finite value that fits binary32, as bits: 24 mantissa bits when normal, fewer at the smallest exponent when subnormal
def encode
def add
def sub
def mul
def soft
def hard
def HardOkthe hardware assumption: Base's F32.add and F32.mul are correctly rounded

type StepOne step of reading a sequence: nothing left, or an element and the rest.
def uncons
law append_nil
law append_assoc
law reverse_goList.reverse is List.reverse.go(xs, Nil{}); this says what the accumulator does.