Strings

Strings are of the predefined type string. Literal strings are set between double quotes.

const a: string = "Hello Alice";

For reference, see the predefined namespace String.

Casting

Strings can be used in contexts where a boolean is expected: an empty string is interpreted as false and a non-empty string is interpreted as true.

const one = "" ? 0 : 1;

const zero = "foo" ? 0 : 1;

Concatenating

Strings can be concatenated using the overloaded + operator, like so:

const name = "Alice";

const greeting = "Hello";

const full_greeting = greeting + " " + name;

Sizing

To get the length of a string, use the function String.length or String.size:

const length : nat = String.size("Alice"); // length == (5 as nat)

Slicing

You can extract a substring from a string with the String.sub function. It accepts a nat for the index of the start of the substring and a nat for the number of characters. Both numbers are inclusive. The first character of a string has the index 0.

The offset and length of the slice are natural number:

const name = "Alice";

const slice = String.sub (0 as nat, 1 as nat, name); // slice == "A"

Verbatim strings

Strings can contain control characters, like \n. To interpret each character on its own (such as treating \n as two characters), you can either escape the backslash character or use verbatim strings. Verbatim strings have the same type as ordinary strings (that is, interpreted strings).

Verbatim strings are given between backquotes (a.k.a. backticks), instead of double quotes:

const s : string = `\n` // String made of two characters