Standard library

Every function below is written in Velaris and parsed onto this page by the real compiler — contracts included. A violated requires is a compile error at your call site.

fn first(xs: List of T) -> T for any T
requires length(xs) > 0
fn last(xs: List of T) -> T for any T
requires length(xs) > 0
fn reverse(xs: List of T) -> List of T for any T
fn index_of(xs: List of T, item: T) -> Int for any T
fn contains_item(xs: List of T, item: T) -> Bool for any T
fn apply_to_each(xs: List of T, f: fn(T) -> T) -> List of T for any T
fn keep_if(xs: List of T, keep: fn(T) -> Bool) -> List of T for any T
fn count_where(xs: List of T, keep: fn(T) -> Bool) -> Int for any T
fn sum_of(xs: List of Int) -> Int
fn max_of(xs: List of Int) -> Int
requires length(xs) > 0
ensures contains_item(xs, result)
fn min_of(xs: List of Int) -> Int
requires length(xs) > 0
ensures contains_item(xs, result)
fn is_sorted(xs: List of Int) -> Bool
fn insert_sorted(xs: List of Int, v: Int) -> List of Int
fn sort(xs: List of Int) -> List of Int
ensures length(result) == length(xs)
ensures is_sorted(result)
fn insert_by(xs: List of T, v: T, key: fn(T) -> Int) -> List of T for any T
fn sort_by(xs: List of T, key: fn(T) -> Int) -> List of T for any T
ensures length(result) == length(xs)
fn join(xs: List of Text, sep: Text) -> Text
fn range_list(a: Int, b: Int) -> List of Int

Built-in functions

NameEffectsTakesGives
all_ofpureAny, AnyBool
any_ofpureAny, AnyBool
argsioList of Text
askioTextText
charspureTextList of Text
code_atpureText, IntInt
containspureText, TextBool
fetch or failnetTextText
fetch_status or failnetTextInt
file_existsfsTextBool
formatpureAnyText
getpureAny, AnyAny
get_orpureAny, Any, AnyAny
haspureAny, AnyBool
json_float or failpureText, TextFloat
json_get or failpureText, TextText
json_haspureText, TextBool
json_int or failpureText, TextInt
json_len or failpureText, TextInt
json_ofpureAnyText
keyspureAnyAny
lengthpureAnyInt
lowerpureTextText
nowclockInt
post or failnetText, TextText
printioAnyUnit
pushpureAny, AnyAny
putpureAny, Any, AnyAny
py or failffiText, Text, List of TextText
py_closeffiHandleUnit
py_do or failffiHandle, Text, TextText
py_field or failffiHandle, TextText
py_float or failffiText, Text, List of TextFloat
py_int or failffiText, Text, List of TextInt
py_json or failffiText, Text, TextText
py_new or failffiText, Text, TextHandle
randomrandIntInt
read_file or failfsTextText
roundpureFloatInt
splitpureText, TextList of Text
to_floatpureIntFloat
to_int or failpureTextInt
to_textpureAnyText
upperpureTextText
write_filefsText, AnyUnit

get on a map can also fail (missing key); get_or never fails.