string

Strings of characters

length: (_: string) => nat

The call String.length(s) is the number of characters in the string s. Note: String.length is another name for String.size.

size: (_: string) => nat

The call String.size(s) is the number of characters in the string s.

concat: (left: string, right: string) => string

The call String.concat(left, right) is the concatenation of the string left and the string right, in that order.

concats: (list: list<string>) => string

The call String.concats(list) is the concatenation of the strings in the list list, from left to right.

sub: (index: nat, length: nat, string: string) => string

The call String.sub(index, len, str) is the substring of string str starting at index index (0 denoting the first character) and of length len. If the index or length are invalid, an exception interrupts the execution.

slice: (index: nat, length: nat, string: string) => string

The call String.slice(index, len, str) is the substring of string str starting at index index (0 denoting the first character) and of length len. If the index or length are invalid, an exception interrupts the execution.