Skip to content
Kavachकवच

Standard Library: std.math

● Intermediate5 min

Every type, method and function of std.math: what the spec lists, then each declaration in its source, with its examples and the line that declares it.

Spec 14.5 · learn it in Math.

A declaration below shows what a program writes against: a type's fields, a function's parameters, what it gives, its contracts (require, ensure) and its examples. kavach test runs every example, so each one is true of the code.

spec 14.5 · std.maththe examples, tested

What the spec lists

NameGives
math.pi, math.eThe constants, as Float
math.sqrt(x), math.pow(x, y)For Float or Float32, giving the same type; a Float32 is worked out as a Float and rounded once
math.floor(x), math.ceil(x), math.round(x)The same; round rounds halves away from zero
math.gcd(a, b), math.lcm(a, b)Greatest common divisor and least common multiple of Ints
math.is_prime(n)Whether n is a prime number
math.factorial(n)n! for 0 <= n <= 20 (larger values don't fit in Int)
math.mean(xs)The average of a [Float], or none for an empty list

std.math · math.kav

use std.math: 0 types and 5 functions. stdlib/math/math.kav

gcd function

The greatest common divisor of two numbers that are not negative.

pub fn gcd(a: Int, b: Int) -> Int
    require a >= 0
    require b >= 0
    ensure result >= 0
    example gcd(12, 18) == 6
    example gcd(0, 5) == 5
    example gcd(7, 0) == 7

lcm function

The least common multiple, or none when it doesn't fit in Int.

pub fn lcm(a: Int, b: Int) -> Int?
    require a >= 0
    require b >= 0
    example lcm(4, 6) == 12
    example lcm(0, 5) == 0
    example lcm(9_223_372_036_854_775_807, 2) == none

factorial function

n! for 0 <= n <= 20; larger values don't fit in Int.

pub fn factorial(n: Int) -> Int
    require n >= 0
    require n <= 20
    ensure result >= 1
    example factorial(0) == 1
    example factorial(5) == 120
    example factorial(20) == 2_432_902_008_176_640_000

mean function

The average of the numbers, or none for an empty list.

pub fn mean(xs: [Float]) -> Float?
    example mean([1.0, 2.0, 6.0]) == 3.0
    example mean([]) == none

is_prime function

Whether n is prime. A Miller-Rabin test with fixed bases, which is exact for every Int and takes microseconds even for the largest.

pub fn is_prime(n: Int) -> Bool
    example is_prime(2)
    example is_prime(97)
    example not is_prime(1)
    example not is_prime(91)
    example is_prime(1_000_000_007)
    example is_prime(9_223_372_036_854_775_783)
    example not is_prime(9_223_372_036_854_775_807)