This module defines the necessary instances to register Char → Bool with the pattern framework.

@[instance_reducible, defaultInstance 1000]

instance String.Slice.Pattern.CharPred.instForwardPatternForallCharBool {p : Char → Bool} : ForwardPattern p

Equations

• One or more equations did not get rendered due to their size.

instance String.Slice.Pattern.CharPred.instStrictForwardPatternForallCharBool {p : Char → Bool} : StrictForwardPattern p

instance String.Slice.Pattern.CharPred.instLawfulForwardPatternForallCharBool {p : Char → Bool} : LawfulForwardPattern p

@[instance_reducible, defaultInstance 1000]

instance String.Slice.Pattern.CharPred.instToForwardSearcherForallCharBoolDefaultForwardSearcher {p : Char → Bool} : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher p)

Equations

• String.Slice.Pattern.CharPred.instToForwardSearcherForallCharBoolDefaultForwardSearcher = String.Slice.Pattern.ToForwardSearcher.defaultImplementation

@[instance_reducible]

instance String.Slice.Pattern.CharPred.Decidable.instForwardPatternForallCharPropOfDecidablePred {p : Char → Prop} [DecidablePred p] : ForwardPattern p

Equations

• One or more equations did not get rendered due to their size.

instance String.Slice.Pattern.CharPred.Decidable.instStrictForwardPatternForallCharProp {p : Char → Prop} [DecidablePred p] : StrictForwardPattern p

instance String.Slice.Pattern.CharPred.Decidable.instLawfulForwardPatternForallCharProp {p : Char → Prop} [DecidablePred p] : LawfulForwardPattern p

@[instance_reducible]

instance String.Slice.Pattern.CharPred.Decidable.instToForwardSearcherForallCharPropDefaultForwardSearcherForallBoolDecide {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher fun (x : Char) => decide (p x))

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible, defaultInstance 1000]

instance String.Slice.Pattern.CharPred.instBackwardPatternForallCharBool {p : Char → Bool} : BackwardPattern p

Equations

• One or more equations did not get rendered due to their size.

instance String.Slice.Pattern.CharPred.instStrictBackwardPatternForallCharBool {p : Char → Bool} : StrictBackwardPattern p

instance String.Slice.Pattern.CharPred.instLawfulBackwardPatternForallCharBool {p : Char → Bool} : LawfulBackwardPattern p

@[instance_reducible, defaultInstance 1000]

instance String.Slice.Pattern.CharPred.instToBackwardSearcherForallCharBoolDefaultBackwardSearcher {p : Char → Bool} : ToBackwardSearcher p (ToBackwardSearcher.DefaultBackwardSearcher p)

Equations

• String.Slice.Pattern.CharPred.instToBackwardSearcherForallCharBoolDefaultBackwardSearcher = String.Slice.Pattern.ToBackwardSearcher.defaultImplementation

@[instance_reducible]

instance String.Slice.Pattern.CharPred.Decidable.instBackwardPatternForallCharPropOfDecidablePred {p : Char → Prop} [DecidablePred p] : BackwardPattern p

Equations

• One or more equations did not get rendered due to their size.

instance String.Slice.Pattern.CharPred.Decidable.instStrictBackwardPatternForallCharProp {p : Char → Prop} [DecidablePred p] : StrictBackwardPattern p

instance String.Slice.Pattern.CharPred.Decidable.instLawfulBackwardPatternForallCharProp {p : Char → Prop} [DecidablePred p] : LawfulBackwardPattern p

@[instance_reducible]

instance String.Slice.Pattern.CharPred.Decidable.instToBackwardSearcherForallCharPropDefaultBackwardSearcherForallBoolDecide {p : Char → Prop} [DecidablePred p] : ToBackwardSearcher p (ToBackwardSearcher.DefaultBackwardSearcher fun (x : Char) => decide (p x))

Equations

• One or more equations did not get rendered due to their size.