Commit 2024-06-05 08:10 c1e640b7

View on Github →

chore: fix names for String lemmas (#13525)

Estimated changes

Modified Mathlib/Data/String/Basic.lean

modified theorem List.asString_eq

modified theorem List.asString_inj

modified theorem List.length_asString

added theorem List.toList_asString

deleted theorem List.toList_inv_asString

deleted theorem String.asString_inv_toList

added theorem String.asString_nil

added theorem String.asString_toList

deleted theorem String.nil_asString_eq_empty

Modified Mathlib/Data/String/Defs.lean

deleted def String.getRest