Documentation

Init.Data.String.Length

ā† Copula mathematical handbook
source
@[extern lean_string_length]
def String.length (b : String) :
Nat

Returns the length of a string in Unicode code points.

Examples:

Equations
Instances For
    source
    @[simp]
    theorem String.Internal.size_toArray {b : String} :
    (toArray b).size = b.length
    source
    theorem String.length_toList {s : String} :
    s.toList.length = s.length
    source
    @[deprecated String.length_toList (since := "2025-10-30")]
    theorem String.length_data {b : String} :
    b.toList.length = b.length
    source
    @[simp]
    theorem String.length_ofList {l : List Char} :
    (ofList l).length = l.length
    source
    @[deprecated String.length_ofList (since := "2025-10-30")]
    theorem List.length_asString {l : List Char} :
    (String.ofList l).length = l.length
    source
    @[simp]
    theorem String.length_empty :
    "".length = 0
    source
    @[simp]
    theorem String.length_singleton {c : Char} :
    (singleton c).length = 1
    source
    @[simp]
    theorem String.length_push {s : String} (c : Char) :
    (s.push c).length = s.length + 1
    source
    @[simp]
    theorem String.length_pushn {s : String} (c : Char) (n : Nat) :
    (s.pushn c n).length = s.length + n
    source
    @[simp]
    theorem String.length_append (s t : String) :
    (s ++ t).length = s.length + t.length
    source
    @[deprecated String.length_singleton (since := "2026-02-12")]
    theorem Char.length_toString (c : Char) :
    c.toString.length = 1