Math

Table of Contents

Functions

math

def math : Unit

PI

The value of PI (3.14159265...), bounded to a tight range so refinements can reason about it (e.g. that it is positive and that 3 < PI < 4).
def PI : {v : Float | 3.1415926 < v && v < 3.1415927}

E

The value of Euler's number e (2.71828182...).
def E : {v : Float | 2.7182818 < v && v < 2.7182819}

TAU

The value of tau (2 * PI, 6.28318530...).
def TAU : {v : Float | 6.2831853 < v && v < 6.2831854}

INF

Positive infinity.
def INF : Float

toFloat

Converts an integer to a float.
def toFloat (i : Int) : Float

toInt

Converts a float to an integer (truncates towards zero).
def toInt (i : Float) : Int

min

Returns the minimum of two integers.
def min (i : Int) (j : Int) : Int

max

Returns the maximum of two integers.
def max (i : Int) (j : Int) : Int

abs

Returns the absolute value of an integer.
def abs (i : Int) : {v : Int | v ≥ 0}

pow

Raises an integer to the power of a non-negative integer.
def pow (i : Int) (j : Int | j ≥ 0) : Int

floor_division

Performs integer division (floor division). Divisor must be nonzero.
def floor_division (i : Int) (j : Int | j ≠ 0) : Int

gcd

Returns the greatest common divisor of two integers.
def gcd (i : Int) (j : Int) : {v : Int | v ≥ 0}

lcm

Returns the least common multiple of two integers.
def lcm (i : Int) (j : Int) : {v : Int | v ≥ 0}

factorial

Returns the factorial of a non-negative integer.
def factorial (i : Int | i ≥ 0) : {v : Int | v ≥ 1}

comb

Returns n choose k (binomial coefficient).
def comb (n : Int | n ≥ 0) (k : Int | k ≥ 0) : {v : Int | v ≥ 0}

perm

Returns n permute k (number of permutations).
def perm (n : Int | n ≥ 0) (k : Int | k ≥ 0) : {v : Int | v ≥ 0}

minf

Returns the minimum of two floats.
def minf (i : Float) (j : Float) : Float

maxf

Returns the maximum of two floats.
def maxf (i : Float) (j : Float) : Float

absf

Returns the absolute value of a float.
def absf (i : Float) : {v : Float | v ≥ 0.0}

powf

Raises a float to the power of another float.
def powf (i : Float) (j : Float) : Float

remainder

Returns the remainder of i / j (IEEE 754 style).
def remainder (i : Float) (j : Float | j ≠ 0.0) : Float

fmod

Returns the float modulo.
def fmod (i : Float) (j : Float | j ≠ 0.0) : Float

round

Rounds a float to the nearest integer.
def round (i : Float) : Int

ceil

Returns the ceiling of a float as an integer.
def ceil (i : Float) : Int

floor

Returns the floor of a float as an integer.
def floor (i : Float) : Int

trunc

Truncates a float to an integer (towards zero).
def trunc (i : Float) : Int

sqrt

Returns the square root of a non-negative integer as a float.
def sqrt (i : Int | i ≥ 0) : {v : Float | v ≥ 0.0}

sqrtf

Returns the square root of a non-negative float.
def sqrtf (i : Float | i ≥ 0.0) : {v : Float | v ≥ 0.0}

isqrt

Returns the integer square root of a non-negative integer.
def isqrt (i : Int | i ≥ 0) : {v : Int | v ≥ 0}

cbrt

Returns the cube root of a float.
def cbrt (i : Float) : Float

exp

Returns e raised to the power of the given float.
def exp (i : Float) : {v : Float | v > 0.0}

expm1

Returns e**x - 1, more precise for small x.
def expm1 (i : Float) : Float

exp2

Returns 2 raised to the power of the given float.
def exp2 (i : Float) : {v : Float | v > 0.0}

log

Returns the natural logarithm (base e) of a positive float.
def log (i : Float | i > 0.0) : Float

log10

Returns the base-10 logarithm of a positive float.
def log10 (i : Float | i > 0.0) : Float

log2

Returns the base-2 logarithm of a positive float.
def log2 (i : Float | i > 0.0) : Float

log1p

Returns log(1 + x), more precise for small x.
def log1p (i : Float | i > -1.0) : Float

sin

Returns the sine of a float (in radians).
def sin (i : Float) : Float

cos

Returns the cosine of a float (in radians).
def cos (i : Float) : Float

tan

Returns the tangent of a float (in radians).
def tan (i : Float) : Float

asin

Returns the arc sine of a float in [-1, 1].
def asin (i : Float | -1.0 ≤ i && i ≤ 1.0) : Float

acos

Returns the arc cosine of a float in [-1, 1].
def acos (i : Float | -1.0 ≤ i && i ≤ 1.0) : Float

atan

Returns the arc tangent of a float.
def atan (i : Float) : Float

atan2

Returns the arc tangent of sinVal/cosVal, in radians.
def atan2 (sinVal : Float) (cosVal : Float) : Float

radians

Converts degrees to radians.
def radians (deg : Float) : Float

degrees

Converts radians to degrees.
def degrees (rad : Float) : Float

hypot

Returns the Euclidean distance between two 2D points.
def hypot (x : Float) (y : Float) : {v : Float | v ≥ 0.0}

sinh

Returns the hyperbolic sine.
def sinh (i : Float) : Float

cosh

Returns the hyperbolic cosine. Result is always >= 1.
def cosh (i : Float) : {v : Float | v ≥ 1.0}

tanh

Returns the hyperbolic tangent.
def tanh (i : Float) : Float

asinh

Returns the inverse hyperbolic sine.
def asinh (i : Float) : Float

acosh

Returns the inverse hyperbolic cosine. Input must be >= 1.
def acosh (i : Float | i ≥ 1.0) : {v : Float | v ≥ 0.0}

atanh

Returns the inverse hyperbolic tangent. Input must be in (-1, 1).
def atanh (i : Float | -1.0 < i && i < 1.0) : Float

erf

Returns the error function.
def erf (i : Float) : Float

erfc

Returns the complementary error function.
def erfc (i : Float) : Float

lgamma

Returns the natural log of the absolute value of the Gamma function.
def lgamma (i : Float) : Float

gamma

Returns the Gamma function. Input must be positive or non-integer.
def gamma (i : Float | i > 0.0) : {v : Float | v > 0.0}

isfinite

Returns true if the float is finite (not infinity or NaN).
def isfinite (i : Float) : Bool

isinf

Returns true if the float is infinity.
def isinf (i : Float) : Bool

isnan

Returns true if the float is NaN.
def isnan (i : Float) : Bool

sign

Returns the sign of an integer: -1, 0, or 1.
def sign (i : Int) : {v : Int | v ≥ 0 - 1 && v ≤ 1}

signf

Returns the sign of a float: -1, 0, or 1.
def signf (i : Float) : {v : Int | v ≥ 0 - 1 && v ≤ 1}

clamp

Clamps an integer to the range [lo, hi].
def clamp (x : Int) (lo : Int) (hi : Int | hi ≥ lo) : {v : Int | v ≥ lo && v ≤ hi}

clampf

Clamps a float to the range [lo, hi].
def clampf (x : Float) (lo : Float) (hi : Float | hi ≥ lo) : {v : Float | v ≥ lo && v ≤ hi}