String

Imports
open Array;
Table of Contents

Types

String

(type)
type String

Functions

len

Returns the length of the string.
def len (i : String) : Int

intToString

Converts an integer to a string.
def intToString (i : Int) : String

equal

Checks if two strings are equal.
def equal : (i : String) → (j : String) → Bool

slice

Returns a substring (slice) of the string from index j to l (exclusive).
def slice : (i : String) → (j : Int | j ≥ 0 && j < len i) → (l : Int | l ≥ j && l ≤ len i) → String

upper

Converts the string to uppercase.
def upper : (i : String) → String

lower

Converts the string to lowercase.
def lower : (i : String) → String

replace

Replaces all occurrences of substring j with l in string i.
def replace (i : String) (j : String | len j > 0) (l : String) : String

split

Splits the string by the given separator.
def split (i : String) (j : String | len j > 0) : Array String

concat

Concatenates two strings.
def concat (i : String) (j : String) : String

startsWith

Checks if the string starts with the given prefix.
def startsWith (i : String) (prefix : String) : Bool

endsWith

Checks if the string ends with the given suffix.
def endsWith (i : String) (suffix : String) : Bool

indexOf

Finds the first index of substring sub in i, or -1 if not found.
def indexOf (i : String) (sub : String) : Int

lastIndexOf

Finds the last index of substring sub in i, or -1 if not found.
def lastIndexOf (i : String) (sub : String) : Int

contains

Checks if the string contains the given substring.
def contains (i : String) (sub : String) : Bool

trim

Removes whitespace from both ends of the string.
def trim (i : String) : String

trimLeft

Removes whitespace from the left end of the string.
def trimLeft (i : String) : String

trimRight

Removes whitespace from the right end of the string.
def trimRight (i : String) : String

repeat

Repeats the string n times.
def repeat (i : String) (n : Int | n ≥ 0) : String

isEmpty

Returns true if the string is empty.
def isEmpty (i : String) : Bool

toCharList

Splits the string into a list of characters.
def toCharList (i : String) : Array String

charAt

Character at index i, or the empty string when i is out of range (str.at).
def charAt (s : String) (i : Int) : String

substr

Substring of length `length` starting at `start` (str.substr); clamps to the empty string for negative arguments, like the SMT-LIB semantics.
def substr (s : String) (start : Int) (length : Int) : String

indexOfFrom

First index of `sub` in `s` at or after `start`, or -1 (str.indexof).
def indexOfFrom (s : String) (sub : String) (start : Int) : Int

stringToInt

Parse the string as an integer, or -1 when it is not a non-negative integer literal (str.to.int).
def stringToInt (s : String) : Int