String operators

length

(length s)

(length s)

• takes s: string
• produces integer

String length

Supported in either invariants or properties.

+

(+ s t)

(+ s t)

• takes s: string
• takes t: string
• produces string

(+ s t)

(+ s t)

• takes s: [a]
• takes t: [a]
• produces [a]

String / list concatenation

Supported in either invariants or properties.

str-to-int

(str-to-int s)

(str-to-int s)

• takes s: string
• produces integer

(str-to-int b s)

(str-to-int b s)

• takes b: integer
• takes s: string
• produces integer

String to integer conversion

Supported in either invariants or properties.

take

(take n s)

(take n s)

• takes n: integer
• takes s: string
• produces string

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

Supported in either invariants or properties.

drop

(drop n s)

(drop n s)

• takes n: integer
• takes s: string
• produces string

drop the first n values from xs (dropped from the end if n is negative)

Supported in either invariants or properties.

hash

(hash s)

(hash s)

• takes s: string
• produces string

BLAKE2b 256-bit hash of string values

Supported in properties only.

hash

(hash s)

(hash s)

• takes s: a
• produces string
• where a is of type integer or decimal

BLAKE2b 256-bit hash of numerical values

Supported in properties only.