Strings

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

const a :string = "Hello Alice";

Note: See predefined namespace String

Casting

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

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;

Note: See predefined namespace String

Sizing

The length of a string can be obtain by calling the predefined functions String.length or String.size:

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

Note: See predefined namespace String

Slicing

Substrings can be extracted using the predefined function String.sub. The first character has index 0 and the interval of indices for the substring has inclusive bounds.

The offset and length of the slice are natural number:

const name = "Alice";

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

Note: See predefined namespace String

Verbatim

Strings can contain control characters, like \n. Sometimes we need that each character in a string is interpreted on its own, for example \n as two characters instead of a newline character. In that case, either we escape the backslash character, or we use verbatim strings. Those have the same type string as normal (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

Note: See predefined namespace String