num.bend checks
raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/num.bend as Num
2 imports
import Base import ./math.bend as Math
Laws
law catalan_4 provedsource · line 107 · raw
{catalan(4) == 14 : U32}
law perm_5_2 provedsource · line 126 · raw
{perm(5, 2) == 20 : U32}
law prime_nth_6 provedsource · line 146 · raw
{prime_nth(25n, 6) == 13 : U32}
law prime_11 provedsource · line 152 · raw
{is_prime(11) == True{} : Bool}
law prime_9_false provedsource · line 158 · raw
{is_prime(9) == False{} : Bool}
Definitions
def divides source · line 11 · raw
@+d:U32 -> @+n:U32 -> Bool
divides: d | n. divides(0, n) is (n == 0) by convention.
def prime_go source · line 16 · raw
@fuel:Nat -> @+d:U32 -> @+n:U32 -> @bad:Bool -> Bool
is_prime: trial division up to isqrt(n). Fixed (sqrt(n)-1) steps.
def is_prime source · line 23 · raw
@+n:U32 -> Bool
def pi_go source · line 28 · raw
@fuel:Nat -> @+k:U32 -> @acc:U32 -> U32
prime_pi: count of primes 2 <= k <= n.
def prime_pi source · line 36 · raw
@+n:U32 -> U32
def modpow_go source · line 40 · raw
@fuel:Nat -> @+base:U32 -> @+exp:U32 -> @+acc:U32 -> @+m:U32 -> U32
mod_pow: base^exp mod m (m >= 1). Binary method, fixed 32 steps.
def mod_pow source · line 53 · raw
@+base:U32 -> @+exp:U32 -> @+m:U32 -> U32
def coprime source · line 57 · raw
@+a:U32 -> @+b:U32 -> Bool
coprime: gcd(a, b) == 1.
def phi_go source · line 61 · raw
@fuel:Nat -> @+k:U32 -> @+n:U32 -> @acc:U32 -> U32
phi: Euler totient, count of 1 <= k <= n with gcd(k, n) == 1.
def phi source · line 69 · raw
@+n:U32 -> U32
def is_square source · line 73 · raw
@+n:U32 -> Bool
is_square: n is a perfect square.
def icbrt_go source · line 77 · raw
@fuel:Nat -> @+n:U32 -> @+x:U32 -> U32
icbrt: floor(cbrt(n)). Integer Newton, fixed 32 steps, frozen when stable.
def icbrt source · line 86 · raw
@+n:U32 -> U32
def choose_go source · line 90 · raw
@fuel:Nat -> @+i:U32 -> @+n:U32 -> @+k:U32 -> @acc:U32 -> U32
choose: n over k (0 when k > n). Multiplicative, exact for small values.
def choose source · line 98 · raw
@+n:U32 -> @+k:U32 -> U32
def catalan source · line 104 · raw
@+n:U32 -> U32
catalan: choose(2n, n) / (n + 1). Exact for small n.
def perm_go source · line 114 · raw
@fuel:Nat -> @+i:U32 -> @+n:U32 -> @+k:U32 -> @acc:U32 -> U32
perm: falling product n * (n-1) * ... * (n-k+1), 0 when k > n.
def perm source · line 122 · raw
@+n:U32 -> @+k:U32 -> U32
def nth_go source · line 133 · raw
@fuel:Nat -> @+c:U32 -> @+want:U32 -> @cnt:U32 -> @+best:U32 -> U32
prime_nth: value of the want-th prime (1-indexed), fuel-bounded search.
def prime_nth source · line 143 · raw
@fuel:Nat -> @+want:U32 -> U32