Verification of KMP string search #
In this file, we instantiate LawfulToForwardSearcherModel for Slice patterns, which amounts to
verifying that our implementation of KMP string search in Init.Data.String.Pattern.String is
correct.
theorem
String.Slice.Pattern.Model.ForwardSliceSearcher.lawfulToForwardSearcherModel
{pat : Slice}
(hpat : pat.isEmpty = false)
: