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

@[instance_reducible]

instance String.Slice.Pattern.Char.instForwardPatternChar {c : Char} : ForwardPattern c

Equations

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

instance String.Slice.Pattern.Char.instStrictForwardPatternChar {c : Char} : StrictForwardPattern c

instance String.Slice.Pattern.Char.instLawfulForwardPatternChar {c : Char} : LawfulForwardPattern c

@[instance_reducible]

instance String.Slice.Pattern.Char.instToForwardSearcherCharDefaultForwardSearcherForallBoolBeq {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearcher fun (x : Char) => x == c)

Equations

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

@[instance_reducible]

instance String.Slice.Pattern.Char.instBackwardPatternChar {c : Char} : BackwardPattern c

Equations

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

instance String.Slice.Pattern.Char.instStrictBackwardPatternChar {c : Char} : StrictBackwardPattern c

instance String.Slice.Pattern.Char.instLawfulBackwardPatternChar {c : Char} : LawfulBackwardPattern c

@[instance_reducible]

instance String.Slice.Pattern.Char.instToBackwardSearcherCharDefaultBackwardSearcherForallBoolBeq {c : Char} : ToBackwardSearcher c (ToBackwardSearcher.DefaultBackwardSearcher fun (x : Char) => x == c)

Equations

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