Commit 2023-04-30 23:31 27ba1681

View on Github →

chore: move theorems on String to std4 (#3712) https://github.com/leanprover/std4/pull/124 moves the following from Mathlib4 to Std4:

helper simp theorems on String.Pos
String.utf8GetAux.inductionOn

Estimated changes

Modified Mathlib/Data/String/Basic.lean

modified theorem String.Iterator.hasNext.cons_add_csize

deleted theorem String.Pos.byteIdx_zero

deleted theorem String.Pos.eq_iff

deleted theorem String.Pos.zero_add_char

deleted theorem String.Pos.zero_add_string

modified theorem String.get.cons_add_csize

modified theorem String.ltb.cons_add_csize

deleted def String.utf8GetAux.inductionOn.{u}

Modified lake-manifest.json