spec/math/w64.bend checks

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

5 imports

import Base
import ../lib/common.bend as C
import ../../src/math/u64.bend as W
import ../../src/math/w64.bend as X
import ../../src/math/natural.bend as M

Definitions

def value source · line 35 · raw

@a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Nat

def of_nat source · line 41 · raw

@+n:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

the U64 of a value below 2^64

def Mul32.value source · line 44 · raw

@+a:U32 -> @+b:U32 -> Type

def Add.value source · line 47 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def AddOver.value source · line 50 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def Sub.value source · line 53 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:{Nat.is_le(value(b), value(a)) == True{} : Bool} -> Type

def Mul.value source · line 56 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def MulOver.value source · line 59 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def Half.value source · line 62 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def Odd.value source · line 65 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def Lt.value source · line 68 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def Le.value source · line 71 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def Eq.value source · line 74 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def IsZero.value source · line 77 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def Div32.quot source · line 80 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> Type

def Div32.rem source · line 83 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> Type

def Mod32.value source · line 86 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> Type

def DivMod.quot source · line 89 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(b) == False{} : Bool} -> Type

def DivMod.rem source · line 92 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(b) == False{} : Bool} -> Type

def MulMod.value source · line 96 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ha:{Nat.is_lt(value(a), value(m)) == True{} : Bool} -> @+hb:{Nat.is_lt(value(b), value(m)) == True{} : Bool} -> Type

a, b < m: the product reduced, with no 64-bit overflow on the way

def Isqrt.value source · line 100 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

the integer square root of the proved Nat reference

def Isqrt32.value source · line 103 · raw

@+x:U32 -> Type

def Shl.value source · line 106 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+hk:{Nat.is_lt(k, 64n) == True{} : Bool} -> Type

def Shr.value source · line 109 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> Type

def jam source · line 114 · raw

@+q:Nat -> @+r:Nat -> Nat

shifted right, with the shifted-out bits OR-ed into bit 0 (SoftFloat's softfloat_shiftRightJam64); jam(q, r) sets q's bit 0 when r is nonzero

def ShrJam.value source · line 117 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> Type

def Clz.value source · line 121 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

64 for zero