src/float/num.bend checks

raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/num.bend as Num

2 imports

import Base
import ./format.bend as Fmt

Types

type Impl source · line 16 · raw

@-T:Data -> Type

Impl

@-T:Data -> @fmt:0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/format.Format -> @value:(@_:T -> 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/format.Val) -> @add:(@_:T -> @_:T -> T) -> @mul:(@_:T -> @_:T -> T) -> Impl<T>

type Correct source · line 48 · raw

@-T:Data -> @-i:Impl<T> -> Type

an implementation that is correctly rounded everywhere

Correct

@-T:Data -> @-i:Impl<T> -> @add:(@a:T -> @b:T -> AddOk(T, i, a, b)) -> @mul:(@a:T -> @b:T -> MulOk(T, i, a, b)) -> Correct<T, i>

Definitions

def Impl.fmt source · line 19 · raw

@-T:Data -> @i:Impl<T> -> 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/format.Format

def Impl.value source · line 24 · raw

@-T:Data -> @i:Impl<T> -> @x:T -> 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/format.Val

def Impl.add source · line 29 · raw

@-T:Data -> @i:Impl<T> -> @a:T -> @b:T -> T

def Impl.mul source · line 34 · raw

@-T:Data -> @i:Impl<T> -> @a:T -> @b:T -> T

Templates

template AddOk source · line 40 · raw

@-T:Data -> @-i:Impl<T> -> @a:T -> @b:T -> Type

add is correctly rounded at a and b

template MulOk source · line 44 · raw

@-T:Data -> @-i:Impl<T> -> @a:T -> @b:T -> Type

mul is correctly rounded at a and b