Strings

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

const a : string = "Hello Alice"

Concatenating Strings

Strings can be concatenated using the ^ operator.

const name : string = "Alice"

const greeting : string = "Hello"

const 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.

const name : string = "Alice"

const slice : string = String.sub (0n, 1n, name)

Note that string_slide is deprecated.

⚠️ 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:

const name : string = "Alice"

const length : nat = String.length (name) // length = 5

Note that size is deprecated.