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