Version: 0.19.0

Strings

Strings are defined using the built-in string type like this:

let a: string = "Hello Alice";

or with single quotes:

let a: string = 'Hello Alice';

Concatenating Strings#

Strings can be concatenated using the + operator.

let name: string = "Alice";
let greeting: string = "Hello";
let full_greeting: string = greeting + " " + name;

Extracting Subtrings#

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.

let name: string = "Alice";
let slice: string = String.sub (0 as nat, 1 as nat, name);

⚠️ Notice that the offset and length of the slice are natural numbers.

Length of Strings#

The length of a string can be found using a built-in function:

let name: string = "Alice";
let length: nat = String.length(name); // length == 5