~/bend-docscommunity

spec/math/natural.bend checks

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

3 imports
import Base
import ../lib/common.bend as C
import ../../src/math/natural.bend as M

Definitions

def factorial source · line 52 · raw

@n:Nat -> Nat

Mathlib/Data/Nat/Factorial/Basic (Nat.factorial_succ)

def desc source · line 60 · raw

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

n.descFactorial k: (n - k) * n.descFactorial k at k + 1

def choose source · line 68 · raw

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

Mathlib/Data/Nat/Choose/Basic (Pascal's rule, Nat.choose_succ_succ)

def lsum source · line 80 · raw

@xs:List<&2, Nat> -> Nat

List.sum and List.prod as right folds

def lprod source · line 87 · raw

@xs:List<&2, Nat> -> Nat

def dvd source · line 95 · raw

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

d divides a: a quotient k with a == k d (Mathlib's Dvd on Nat)

def nth0 source · line 99 · raw

@+xs:List<&2, Nat> -> @+i:Nat -> @+dflt:Nat -> Nat

xs[i], or dflt past the end

def dvd_with source · line 109 · raw

@+d:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> Type

d divides every element, with the quotients given: xs[i] == ks[i] d

def mul_with source · line 121 · raw

@+m:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> Type

m is a multiple of every element, with the quotients given: m == ks[i] xs[i]

def Gcd.divides_left source · line 134 · raw

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

def Gcd.divides_right source · line 137 · raw

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

def Gcd.greatest source · line 141 · raw

@+a:Nat -> @+b:Nat -> @+d:Nat -> @+ka:Nat -> @+kb:Nat -> @+ea:{a == Nat.mul(ka, d) : Nat} -> @+eb:{b == Nat.mul(kb, d) : Nat} -> Type

every common divisor divides the gcd

def Gcd.mul_left source · line 144 · raw

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

def Lcm.divides_left source · line 147 · raw

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

def Lcm.divides_right source · line 150 · raw

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

def Lcm.least source · line 154 · raw

@+a:Nat -> @+b:Nat -> @+m:Nat -> @+x:Nat -> @+y:Nat -> @+ex:{m == Nat.mul(x, a) : Nat} -> @+ey:{m == Nat.mul(y, b) : Nat} -> Type

the lcm divides every common multiple

def Lcm.gcd_mul_lcm source · line 157 · raw

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

def GcdAll.divides source · line 162 · raw

@+xs:List<&2, Nat> -> @+i:Nat -> Type

def GcdAll.greatest source · line 165 · raw

@+d:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @h:dvd_with(d, xs, ks) -> Type

def LcmAll.divides source · line 168 · raw

@+xs:List<&2, Nat> -> @+i:Nat -> Type

def LcmAll.least source · line 171 · raw

@+m:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @h:mul_with(m, xs, ks) -> Type

def Sum.value source · line 174 · raw

@+xs:List<&2, Nat> -> Type

def Prod.value source · line 177 · raw

@+xs:List<&2, Nat> -> Type

def Factorial.value source · line 182 · raw

@+n:Nat -> Type

def Perm.value source · line 185 · raw

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

def Perm.self source · line 188 · raw

@+n:Nat -> Type

def Comb.value source · line 191 · raw

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

def Comb.pascal source · line 195 · raw

@+m:Nat -> @+j:Nat -> Type

Pascal's rule on the implementation itself

def Comb.factorials source · line 198 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_le(k, n) == True{} : Bool} -> Type

def Comb.zero source · line 202 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_lt(n, k) == True{} : Bool} -> Type

PDF 8.6: comb(n, k) is 0 for k > n, not an error

def Isqrt.le source · line 207 · raw

@+n:Nat -> Type

def Isqrt.lt_succ source · line 210 · raw

@+n:Nat -> Type

def Iroot.done source · line 214 · raw

@+n:Nat -> @+kp:Nat -> Type

a positive degree always has a root

def Iroot.le source · line 217 · raw

@+n:Nat -> @+kp:Nat -> @+r:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.iroot(n, 1n+kp) == Done{r} : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, Nat>} -> Type

def Iroot.lt_succ source · line 220 · raw

@+n:Nat -> @+kp:Nat -> @+r:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.iroot(n, 1n+kp) == Done{r} : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, Nat>} -> Type

def Iroot.zero_degree source · line 224 · raw

@+n:Nat -> Type

PDF 2.3: the zeroth root is a domain error

def Ilog.done source · line 228 · raw

@+np:Nat -> @+bq:Nat -> Type

a positive argument and a base of at least 2 always have a logarithm

def Ilog.pow_le source · line 231 · raw

@+np:Nat -> @+bq:Nat -> @+r:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog(1n+np, 2n+bq) == Done{r} : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, Nat>} -> Type

def Ilog.lt_pow_succ source · line 234 · raw

@+np:Nat -> @+bq:Nat -> @+r:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog(1n+np, 2n+bq) == Done{r} : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, Nat>} -> Type

def Ilog.zero source · line 238 · raw

@+b:Nat -> Type

PDF 2.3 / 4.5: log(0) is a domain error, as is a base below 2

def Ilog.small_base source · line 241 · raw

@+n:Nat -> @+b:Nat -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> Type

def BitLength.lt source · line 244 · raw

@+n:Nat -> Type

def BitLength.le source · line 247 · raw

@+np:Nat -> Type

def PowMod.value source · line 252 · raw

@+b:Nat -> @+e:Nat -> @+mp:Nat -> Type

def PowMod.zero_modulus source · line 256 · raw

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

PDF 8.7: pow(b, e, 0) raises ValueError; here ZeroDivision

def ModInverse.inverse source · line 259 · raw

@+a:Nat -> @+mp:Nat -> @+x:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.mod_inverse(a, 1n+mp) == Done{x} : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, Nat>} -> Type

def ModInverse.reduced source · line 262 · raw

@+a:Nat -> @+mp:Nat -> @+x:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.mod_inverse(a, 1n+mp) == Done{x} : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, Nat>} -> Type

def ModInverse.not_coprime source · line 266 · raw

@+a:Nat -> @+mp:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.mod_inverse(a, 1n+mp) == Fail{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.NotInvertible{}} : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, Nat>} -> Type

PDF 8.7: no inverse exactly when a and m share a factor g >= 2

def ModInverse.zero_modulus source · line 269 · raw

@+a:Nat -> Type

def DivMod.value source · line 274 · raw

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

def DivMod.euclid source · line 277 · raw

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

def DivMod.rem_lt source · line 280 · raw

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

def DivMod.zero_divisor source · line 284 · raw

@+a:Nat -> Type

PDF 3.1: divmod(a, 0) raises ZeroDivisionError

def Clamp.value source · line 287 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_le(lo, hi) == True{} : Bool} -> Type

def Clamp.ge source · line 290 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_le(lo, hi) == True{} : Bool} -> Type

def Clamp.le source · line 293 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> Type

def Clamp.id source · line 296 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h1:{Nat.is_le(lo, x) == True{} : Bool} -> @+h2:{Nat.is_le(x, hi) == True{} : Bool} -> Type

def Clamp.domain source · line 299 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_lt(hi, lo) == True{} : Bool} -> Type