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!" 17 4 "Nat expected"

@[extern lean_string_from_utf8_unchecked]

constant String.fromUTF8Unchecked (a : ByteArray) :

@[extern lean_string_to_utf8]

constant String.toUTF8 (a : String) :