batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: Add `String.isPrefixOf` theorems

Open tjf801 opened this issue 9 months ago • 1 comments

This PR is a redo of #782, but adds the following:

  • Auxiliary theorems used to prove the theorems below
    • These were already in #782
  • Proof of equivalence between String.isPrefixOf s t and ∃ t, s = p ++ t
    • (This is analogous to how List.IsPrefix is defined.)
  • Proof of equivalence between String.isPrefixOf s t and List.isPrefixOf s.data t.data

tjf801 avatar May 23 '24 17:05 tjf801