2.6 KiB
id | title |
---|---|
strings | Strings |
import Syntax from '@theme/Syntax';
Strings are defined using the built-in string
type like this:
const a : string = "Hello Alice"
let a : string = "Hello Alice"
let 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
Strings can be concatenated using the ^
operator.
let name : string = "Alice"
let greeting : string = "Hello"
let full_greeting : string = greeting ^ " " ^ name
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.
const name : string = "Alice"
const slice : string = String.sub (0n, 1n, name)
Note that
string_slide
is deprecated.
let name : string = "Alice"
let slice : string = String.sub 0n 1n name
Note that
String.slice
is deprecated.
let name : string = "Alice";
let slice : string = String.sub (0n, 1n, name);
Note that
String.slice
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.
let name : string = "Alice"
let length : nat = String.length name // length = 5
Note that
String.size
is deprecated.
let name : string = "Alice";
let length : nat = String.length (name); // length == 5
Note that
String.size
is deprecated.