inductive Regex.Data.Anchor : Type

• start : Anchor
• eos : Anchor
• wordBoundary : Anchor
• nonWordBoundary : Anchor

instance Regex.Data.instDecidableEqAnchor : DecidableEq Anchor

Equations

• Regex.Data.instDecidableEqAnchor x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Regex.Data.instReprAnchor : Repr Anchor

Equations

• Regex.Data.instReprAnchor = { reprPrec := Regex.Data.reprAnchor✝ }

instance Regex.Data.instInhabitedAnchor : Inhabited Anchor

Equations

• Regex.Data.instInhabitedAnchor = { default := Regex.Data.Anchor.start }

instance Regex.Data.instToExprAnchor : Lean.ToExpr Anchor

Equations

• Regex.Data.instToExprAnchor = { toExpr := Regex.Data.toExprAnchor✝, toTypeExpr := Lean.Expr.const `Regex.Data.Anchor [] }

def Regex.Data.Anchor.test (it : String.Iterator) (anchor : Anchor) : Bool

Equations

• Regex.Data.Anchor.test it Regex.Data.Anchor.start = decide (it.pos = 0)
• Regex.Data.Anchor.test it Regex.Data.Anchor.eos = it.atEnd
• Regex.Data.Anchor.test it Regex.Data.Anchor.wordBoundary = it.isAtWordBoundary
• Regex.Data.Anchor.test it Regex.Data.Anchor.nonWordBoundary = it.isAtNonWordBoundary