@[implicit_reducible, defaultInstance 1000]
@[implicit_reducible, defaultInstance 1000]
@[implicit_reducible]
@[implicit_reducible]
instance
String.Slice.Pattern.CharPred.Decidable.instToForwardSearcherForallCharPropDefaultForwardSearcherForallBoolDecide
{p : Char → Prop}
[DecidablePred p]
:
ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher fun (x : Char) => decide (p x))
@[implicit_reducible, defaultInstance 1000]
@[implicit_reducible, defaultInstance 1000]
@[implicit_reducible]
@[implicit_reducible]
instance
String.Slice.Pattern.CharPred.Decidable.instToBackwardSearcherForallCharPropDefaultBackwardSearcherForallBoolDecide
{p : Char → Prop}
[DecidablePred p]
:
ToBackwardSearcher p (ToBackwardSearcher.DefaultBackwardSearcher fun (x : Char) => decide (p x))