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