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 : {x : Int | x ≥ 0 && x < len i}) → (l : {y : Int | y ≥ j && y ≤ 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: {s : String | len s > 0}) (l: String) : String

split

Splits the string by the given separator.
def split (i: String) (j: {s : String | len s > 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: {x : Int | x ≥ 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