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: {v : Int | v >= 0}) : Int

floor_division

Performs integer division (floor division). Divisor must be nonzero.
def floor_division (i: Int) (j: {v : Int | v != 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: {v : Int | v >= 0}) : {v : Int | v >= 1}

comb

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

perm

Returns n permute k (number of permutations).
def perm (n: {v : Int | v >= 0}) (k: {v : Int | v >= 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: {v : Float | v != 0.0}) : Float

fmod

Returns the float modulo.
def fmod (i: Float) (j: {v : Float | v != 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: {v : Int | v >= 0}) : {v : Float | v >= 0.0}

sqrtf

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

isqrt

Returns the integer square root of a non-negative integer.
def isqrt (i: {v : Int | v >= 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: {v : Float | v > 0.0}) : Float

log10

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

log2

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

log1p

Returns log(1 + x), more precise for small x.
def log1p (i: {v : Float | v > -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: {v : Float | -1.0 <= v && v <= 1.0}) : Float

acos

Returns the arc cosine of a float in [-1, 1].
def acos (i: {v : Float | -1.0 <= v && v <= 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: {v : Float | v >= 1.0}) : {v : Float | v >= 0.0}

atanh

Returns the inverse hyperbolic tangent. Input must be in (-1, 1).
def atanh (i: {v : Float | -1.0 < v && v < 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: {v : Float | v > 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: {v : Int | v >= lo}) : {v : Int | v >= lo && v <= hi}

clampf

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