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✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Regex.Data.instReprAnchor : Repr Anchor

Equations

• Regex.Data.instReprAnchor = { reprPrec := Regex.Data.instReprAnchor.repr }

def Regex.Data.instReprAnchor.repr : Anchor → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Regex.Data.instReprAnchor.repr Regex.Data.Anchor.start prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.Data.Anchor.start")).group prec✝
• Regex.Data.instReprAnchor.repr Regex.Data.Anchor.eos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.Data.Anchor.eos")).group prec✝

def Regex.Data.instInhabitedAnchor.default : Anchor

Equations

• Regex.Data.instInhabitedAnchor.default = Regex.Data.Anchor.start

instance Regex.Data.instInhabitedAnchor : Inhabited Anchor

Equations

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

instance Regex.Data.instToExprAnchor : Lean.ToExpr Anchor

Equations

• Regex.Data.instToExprAnchor = { toExpr := Regex.Data.instToExprAnchor.toExpr✝, 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