Utils

@[irreducible]

def Char.multiple (c : Char) (n : Nat) (acc : String) : String

make String with n c chars

Equations

• c.multiple n acc = if n = 0 then acc else c.multiple (n - 1) (c.toString ++ acc)

def Char.isHexDigit (c : Char) : Bool

Equations

• One or more equations did not get rendered due to their size.

def Char.decodeHexDigit (c : Char) : Option UInt32

Equations

• One or more equations did not get rendered due to their size.

def Char.decodeHexDigits (chars : List Char) : Except String UInt32

Equations

• One or more equations did not get rendered due to their size.

def Char.decodeOctDigit (c : Char) : Option UInt32

Equations

• c.decodeOctDigit = if (decide ('0' ≤ c) && decide (c ≤ '7')) = true then some (c.val - '0'.val) else none

def Char.decodeOctDigits (chars : List Char) : Except String UInt32

Equations

• One or more equations did not get rendered due to their size.

def Nat.intAsString (val : Nat) : String

Equations

• One or more equations did not get rendered due to their size.

def UInt32.intAsString (val : UInt32) : String

Equations

• val.intAsString = (↑val.toFin).intAsString

instance String.instCoeSubstring_regex : Coe String Substring

Equations

• String.instCoeSubstring_regex = { coe := fun (s : String) => s.toSubstring }

def String.getAtCodepoint (s : String) (i : Nat) : Char

get i char in s, tood: switch to String.Pos logic

Equations

• s.getAtCodepoint i = if h : i < s.length then s.data.get ⟨i, h⟩ else default

def String.startsAtCodepoint (s m : String) (i : Nat) : Bool

starts string m at codepoint i in s

Equations

• s.startsAtCodepoint m i = if i + m.length ≤ s.length then let s := s.toSubstring.drop i; s.toString.startsWith m else false

def String.toBytePosition (s : String) (p : Nat) : Pos

compute the byte position of the codepoint position p in s

Equations

• s.toBytePosition p = { byteIdx := { data := List.take p s.data }.utf8ByteSize }

def String.toSpan (s : String) (startPos stopPos : Nat) : Substring

make Substring of String

Equations

• s.toSpan startPos stopPos = { str := s, startPos := s.toBytePosition startPos, stopPos := s.toBytePosition stopPos }

def String.decodeHex (s : String) : Except String UInt32

Equations

• s.decodeHex = Char.decodeHexDigits (if s.startsWith "0x" = true then s.replace "0x" "" else s).data

def String.asHex (s : String) : String

Equations

• One or more equations did not get rendered due to their size.