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 csv.fields(line: Text) -> List of Text
ensures length(result) >= 1
fn csv.line_of(values: List of Text) -> Text
fn csv.column(line: Text, at: Int) -> Text or fail
fn csv.column_int(line: Text, at: Int) -> Int or fail
fn csv.rows_of(text: Text) -> List of Text
ensures length(result) >= 1
fn dates.days_in(year: Int, month: Int) -> Int
requires month >= 1
requires month <= 12
ensures result >= 28
ensures result <= 31
fn dates.make(year: Int, month: Int, day: Int) -> Date or fail
fn dates.parse(text: Text) -> Date or fail
fn dates.text_of(d: Date) -> Text
fn dates.before(a: Date, b: Date) -> Bool
fn dates.same(a: Date, b: Date) -> Bool
fn dates.next_day(d: Date) -> Date or fail
requires d.month >= 1
requires d.month <= 12
fn dates.today() -> Date or fail uses ffi
fn db.open(path: Text) -> Handle or fail uses ffi
fn db.run(conn: Handle, sql: Text) -> Text or fail uses ffi
fn db.commit(conn: Handle) or fail uses ffi
fn db.rows_json(conn: Handle, sql: Text) -> Text or fail uses ffi
fn db.count(conn: Handle, table: Text) -> Int or fail uses ffi
ensures result >= 0
fn db.close(conn: Handle) uses ffi
fn env_tools.setting(name: Text, fallback: Text) -> Text uses io
fn env_tools.number_setting(name: Text, fallback: Int) -> Int uses io
fn env_tools.succeed() uses io
fn env_tools.give_up(why: Text) uses io
fn http.get(url: Text) -> Text or fail uses net
fn http.status(url: Text) -> Int or fail uses net
ensures result >= 0
fn http.ok(url: Text) -> Bool or fail uses net
fn http.send(url: Text, body: Text) -> Text or fail uses net
fn http.get_json(url: Text, path: Text) -> Text or fail uses net
fn http.call(method: Text, url: Text, body: Text, headers: Text) -> Text or fail uses net
fn http.body_of(answer: Text) -> Text or fail
fn http.code_of(answer: Text) -> Int or fail
fn http.header_of(answer: Text, name: Text) -> Text or fail
fn http.get_with(url: Text, headers: Text) -> Text or fail uses net
fn http.post_json(url: Text, body: Text) -> Text or fail uses net
fn log.info(message: Text) uses io
fn log.warn(message: Text) uses io
fn log.error(message: Text) uses io
fn log.field(name: Text, value: Text) -> Text
fn log.event(name: Text, details: Text) uses io
fn log.fail_with(message: Text) uses io
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
fn time.today() -> Text or fail uses ffi
fn time.clock_text() -> Text or fail uses ffi
fn time.seconds() -> Int uses clock
fn time.day_of(when: Text) -> Text or fail
fn time.year_of(date: Text) -> Int or fail
fn time.month_of(date: Text) -> Int or fail
fn time.day_number(date: Text) -> Int or fail
Built-in functions
| Name | Effects | Takes | Gives |
|---|---|---|---|
all_of | pure | Any, Any | Bool |
any_of | pure | Any, Any | Bool |
args | io | List of Text | |
ask | io | Text | Text |
chars | pure | Text | List of Text |
code_at | pure | Text, Int | Int |
contains | pure | Text, Text | Bool |
env | io | Text, Text | Text |
exit_with | io | Int | Unit |
fetch or fail | net | Text | Text |
fetch_status or fail | net | Text | Int |
file_exists | fs | Text | Bool |
format | pure | Any | Text |
get | pure | Any, Any | Any |
get_or | pure | Any, Any, Any | Any |
has | pure | Any, Any | Bool |
json_float or fail | pure | Text, Text | Float |
json_get or fail | pure | Text, Text | Text |
json_has | pure | Text, Text | Bool |
json_int or fail | pure | Text, Text | Int |
json_len or fail | pure | Text, Text | Int |
json_of | pure | Any | Text |
keys | pure | Any | Any |
length | pure | Any | Int |
log | io | Any | Unit |
lower | pure | Text | Text |
now | clock | Int | |
post or fail | net | Text, Text | Text |
print | io | Any | Unit |
push | pure | Any, Any | Any |
put | pure | Any, Any, Any | Any |
py or fail | ffi | Text, Text, List of Text | Text |
py_close | ffi | Handle | Unit |
py_do or fail | ffi | Handle, Text, Text | Text |
py_field or fail | ffi | Handle, Text | Text |
py_float or fail | ffi | Text, Text, List of Text | Float |
py_int or fail | ffi | Text, Text, List of Text | Int |
py_json or fail | ffi | Text, Text, Text | Text |
py_new or fail | ffi | Text, Text, Text | Handle |
random | rand | Int | Int |
read_file or fail | fs | Text | Text |
read_line | io | Text | |
request or fail | net | Text, Text, Text, Text | Text |
round | pure | Float | Int |
split | pure | Text, Text | List of Text |
to_float | pure | Int | Float |
to_int or fail | pure | Text | Int |
to_text | pure | Any | Text |
upper | pure | Text | Text |
write_file | fs | Text, Any | Unit |
get on a map can also fail (missing key); get_or never fails.