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

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
`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
`keys`	pure	Any	Any
`length`	pure	Any	Int
`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
`random`	rand	Int	Int
`read_file` or fail	fs	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.