The internal implementation uses dynamic arrays and will perform destructive updates if the String is not shared.
Instances For
The internal implementation uses dynamic arrays and will perform destructive updates if the String is not shared.
Instances For
O(n) in the runtime, where n is the length of the String
Instances For
Equations
- String.utf8GetAux [] x x = default
- String.utf8GetAux (c :: cs) x x = if x = x then c else String.utf8GetAux cs (x + c) x
Instances For
Return character at position p
. If p
is not a valid position
returns (default : Char)
.
See utf8GetAux
for the reference implementation.
Instances For
Equations
- String.utf8GetAux? [] x x = none
- String.utf8GetAux? (c :: cs) x x = if x = x then some c else String.utf8GetAux? cs (x + c) x
Instances For
Instances For
Similar to get
, but produces a panic error message if p
is not a valid String.Pos
.
Instances For
Equations
- String.utf8SetAux c' [] x x = []
- String.utf8SetAux c' (c :: cs) x x = if x = x then c' :: cs else c :: String.utf8SetAux c' cs (x + c) x
Instances For
Instances For
Instances For
Equations
- String.utf8PrevAux [] x x = 0
- String.utf8PrevAux (c :: cs) x x = let i' := x + c; if i' = x then x else String.utf8PrevAux cs i' x
Instances For
Instances For
Similar to get
but runtime does not perform bounds check.
Instances For
Similar to next
but runtime does not perform bounds check.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Returns the first position where the two strings differ.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- String.extract.go₁ [] x x x = []
- String.extract.go₁ (c :: cs) x x x = if x = x then String.extract.go₂ (c :: cs) x x else String.extract.go₁ cs (x + c) x x
Instances For
Equations
- String.extract.go₂ [] x x = []
- String.extract.go₂ (c :: cs) x x = if x = x then [] else c :: String.extract.go₂ cs (x + c) x
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- String.intercalate.go acc s (a :: as) = String.intercalate.go (acc ++ s ++ a) s as
- String.intercalate.go acc s [] = acc
Instances For
- s : String
- i : String.Pos
Iterator for String
. That is, a String
and a position in that string.
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return true
iff the substring of byte size sz
starting at position off1
in s1
is equal to that starting at off2
in s2.
.
False if either substring of that byte size does not exist.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return the codepoint at the given offset into the substring.
Instances For
Given an offset of a codepoint into the substring, return the offset there of the next codepoint.
Instances For
Given an offset of a codepoint into the substring, return the offset there of the previous codepoint.
Instances For
Equations
- Substring.nextn x 0 x = x
- Substring.nextn x (Nat.succ i) x = Substring.nextn x i (Substring.next x x)
Instances For
Equations
- Substring.prevn x 0 x = x
- Substring.prevn x (Nat.succ i) x = Substring.prevn x i (Substring.prev x x)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.