Documentation

Init.Data.String.Extra

def String.toNat! (s : String) :

Equations

String.toNat! s = if String.isNat s = true then String.foldl (fun n c => n * 10 + (Char.toNat c - Char.toNat (Char.ofNat 48))) 0 s else panicWithPosWithDecl "Init.Data.String.Extra" "String.toNat!" 20 4 "Nat expected"

@[extern lean_string_from_utf8_unchecked]

constant String.fromUTF8Unchecked (a : ByteArray) :

Convert a UTF-8 encoded ByteArray string to String. The result is unspecified if a is not properly UTF-8 encoded.

@[extern lean_string_to_utf8]

constant String.toUTF8 (a : String) :

theorem String.one_le_csize (c : Char) :

1 ≤ String.csize c

@[simp]

theorem String.pos_lt_eq (p₁ : String.Pos) (p₂ : String.Pos) :

(p₁ < p₂) = (p₁.byteIdx < p₂.byteIdx)

@[simp]

theorem String.pos_add_char (p : String.Pos) (c : Char) :

(p + c).byteIdx = p.byteIdx + String.csize c

theorem String.eq_empty_of_bsize_eq_zero {s : String} (h : String.endPos s = { byteIdx := 0 }) :

s = ""

theorem String.lt_next (s : String) (i : String.Pos) :

i.byteIdx < (String.next s i).byteIdx

theorem String.Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : String.Iterator.hasNext i = true) :

sizeOf (String.Iterator.next i) < sizeOf i

theorem String.Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬String.Iterator.atEnd i = true) :

sizeOf (String.Iterator.next i) < sizeOf i