disco-0.1.0.0: lib/num.disco

using Primitives

||| Test whether the given natural number is prime.
!!! not (isPrime 0)
!!! not (isPrime 1)
!!! isPrime 2
!!! isPrime 3
!!! isPrime 1000000007
isPrime : N -> Bool
isPrime = $isPrime

||| Takes naturals b and n. Calculates the base b logarithm of n rounded down
!!! log (1,1) == 0
!!! log (3,1) == 0
!!! log (2, 1024) == 10
!!! log (2, 1023) == 9
!!! log (7, 11398895185373143) == 19
log : N * N -> N
log (1,1) = 0
log (0,_) = $crash "Log base 0 is undefined"
log (1,_) = $crash "Log base 1 is undefined for inputs other than 1"
log (_,0) = $crash "Log of Zero"
log (b, x) = {?
                0                   if b > x,
                1 + log (b, x // b) otherwise
              ?}

||| Calculate the base 2 logarithm of the given natural number rounded down
!!! lg 4 == 2
!!! lg 5 == 2
!!! lg 7 == 2
!!! lg 10 == 3
!!! lg 25 == 4
!!! lg 99887766554433221100 == 66
!!! lg (2^100 + 1) == 100
lg : N -> N
lg x = log (2,x)

||| Compute the prime factorization of the given natural number.
factor : N -> Bag(N)
factor = $factor

even : Z -> Bool
even x = 2 divides x

odd : Z -> Bool
odd x = ¬(2 divides x)