2.0 KiB
2.0 KiB
id | title |
---|---|
strings | Strings |
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;
Slicing strings
Strings can be sliced using a built-in function:
const name : string = "Alice"
const slice : string = string_slice (0n, 1n, name)
let name : string = "Alice"
let slice : string = String.slice 0n 1n name
let name : string = "Alice";
let slice : string = String.slice (0n, 1n, name);
⚠️ Notice that the
offset
and slicelength
are natural numbers (nat
).
Aquiring the length of a string
The length of a string can be found using a built-in function:
const name : string = "Alice"
// length = 5
const length : nat = size (name)
let name : string = "Alice"
let length : nat = String.size name
let name : string = "Alice";
let length : nat = String.size (name);