spec/math/number.bend checks

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

4 imports

import Base
import ../lib/common.bend as C
import ../../src/math/natural.bend as M
import ../../src/math/number.bend as NB

Definitions

def ones source · line 21 · raw

@k:Nat -> @+n:Nat -> Nat

the 1 bits among the k lowest bits of n

def BitCount.value source · line 29 · raw

@+n:Nat -> Type

every n is below 2^n, so ones(n, n) counts all of n's 1 bits

def eg_gcd source · line 33 · raw

@r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.EGcd -> Nat

the gcd of the extended algorithm is the proved reference's

def Egcd.gcd source · line 38 · raw

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

def eg_pos source · line 44 · raw

@+a:Nat -> @+b:Nat -> @r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.EGcd -> Nat

the signed Bezout identity a*x - b*y == g (neg false) or b*y - a*x == g (neg true), stated without subtraction: the positive side equals g plus the negative side

def eg_neg source · line 53 · raw

@+a:Nat -> @+b:Nat -> @r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.EGcd -> Nat

def Egcd.bezout source · line 62 · raw

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

def nodiv source · line 66 · raw

@k:Nat -> @+n:Nat -> @+d:Nat -> Bool

no d in [d, d + k) divides n

def prime source · line 74 · raw

@+n:Nat -> Bool

n is prime: 2 <= n and no d in [2, n) divides n

def IsPrime.value source · line 83 · raw

@+n:Nat -> Type