Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-04-05 16:27
0fdb96c1
View on Github →
feat: port Data.String.Basic (
#1054
) mathlib3 SHA: 8a275d92e9f9f3069871cbdf0ddd54b88c17e144
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/String/Basic.lean
added
theorem
List.asString_eq
added
theorem
List.asString_inj
added
theorem
List.length_asString
added
theorem
List.toList_inv_asString
added
theorem
String.Iterator.hasNext.cons_add_csize
added
theorem
String.Pos.byteIdx_zero
added
theorem
String.Pos.eq_iff
added
theorem
String.Pos.zero_add_char
added
theorem
String.Pos.zero_add_string
added
theorem
String.asString_inv_toList
added
theorem
String.get.cons_add_csize
added
theorem
String.head_empty
added
theorem
String.le_iff_toList_le
added
theorem
String.length_toList
added
theorem
String.lt_iff_toList_lt
added
theorem
String.ltb.cons_add_csize
added
def
String.ltb.inductionOn.{u}
added
def
String.ltb
added
theorem
String.nil_asString_eq_empty
added
theorem
String.popn_empty
added
theorem
String.toList_empty
added
theorem
String.toList_inj
added
theorem
String.toList_nonempty
added
theorem
String.toList_singleton
added
def
String.utf8GetAux.inductionOn.{u}
Modified
Mathlib/Data/String/Defs.lean
added
def
String.head
added
def
String.popn