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
ordecimal
BLAKE2b 256-bit hash of numerical values
Supported in properties only.