List operators

at

(at k l)

(at k l)

• takes k: string
• takes l: [a]
• produces a

(at i l)

(at i l)

• takes i: integer
• takes o: list
• produces bool

projection

Supported in either invariants or properties.

length

(length s)

(length s)

• takes s: [a]
• produces integer

List length

Supported in either invariants or properties.

contains

(contains x xs)

(contains x xs)

• takes x: a
• takes xs: [a]
• produces bool

(contains k o)

(contains k o)

• takes k: string
• takes o: object
• produces bool

(contains value string)

(contains value string)

• takes value: string
• takes string: string
• produces bool

List / string / object contains

Supported in either invariants or properties.

enumerate

(enumerate from to step)

(enumerate from to step)

• takes from: integer
• takes to: integer
• takes step: integer
• produces [integer]

Returns a sequence of numbers as a list

Supported in either invariants or properties.

reverse

(reverse xs)

(reverse xs)

• takes xs: [a]
• produces [a]

reverse a list of values

Supported in either invariants or properties.

sort

(sort xs)

(sort xs)

• takes xs: [a]
• produces [a]

sort a list of values

Supported in either invariants or properties.

drop

(drop n xs)

(drop n xs)

• takes n: integer
• takes xs: [a]
• produces [a]

drop the first n values from the beginning of a list (or the end if n is negative)

Supported in either invariants or properties.

take

(take n xs)

(take n xs)

• takes n: integer
• takes xs: [a]
• produces [a]

take the first n values from xs (taken from the end if n is negative)

Supported in either invariants or properties.

make-list

(make-list n a)

(make-list n a)

• takes n: integer
• takes a: a
• produces [a]

create a new list with n copies of a

Supported in either invariants or properties.

map

(map f as)

(map f as)

• takes f: a -> b
• takes as: [a]
• produces [b]

apply f to each element in a list

Supported in either invariants or properties.

filter

(filter f as)

(filter f as)

• takes f: a -> bool
• takes as: [a]
• produces [a]

filter a list by keeping the values for which f returns true

Supported in either invariants or properties.

distinct

(distinct xs)

(distinct xs)

• takes xs: [a]
• produces [a]

returns a list of distinct values

Supported in either invariants or properties.

fold

(fold f a bs)

(fold f a bs)

• takes f: a -> b -> a
• takes a: a
• takes bs: [b]
• produces [a]

reduce a list by applying f to each element and the previous result

Supported in either invariants or properties.

hash

(hash xs)

(hash xs)

• takes xs: [a]
• produces string
• where a is of type integer, decimal, bool, or string

BLAKE2b 256-bit hash of lists

Supported in properties only.