inductive Regex.Data.Anchor : Type

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

@[implicit_reducible]

instance Regex.Data.instDecidableEqAnchor : DecidableEq Anchor

Equations

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

@[implicit_reducible]

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✝

@[implicit_reducible]

instance Regex.Data.instInhabitedAnchor : Inhabited Anchor

Equations

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

def Regex.Data.instInhabitedAnchor.default : Anchor

Equations

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

@[implicit_reducible]

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.instToExprAnchor.toExpr : Anchor → Lean.Expr

Equations

• Regex.Data.instToExprAnchor.toExpr Regex.Data.Anchor.start = Lean.Expr.const `Regex.Data.Anchor.start []
• Regex.Data.instToExprAnchor.toExpr Regex.Data.Anchor.eos = Lean.Expr.const `Regex.Data.Anchor.eos []
• Regex.Data.instToExprAnchor.toExpr Regex.Data.Anchor.wordBoundary = Lean.Expr.const `Regex.Data.Anchor.wordBoundary []
• Regex.Data.instToExprAnchor.toExpr Regex.Data.Anchor.nonWordBoundary = Lean.Expr.const `Regex.Data.Anchor.nonWordBoundary []

def Regex.Data.Anchor.test {s : String} (p : s.Pos) (anchor : Anchor) : Bool

Equations

• Regex.Data.Anchor.test p Regex.Data.Anchor.start = (p == s.startPos)
• Regex.Data.Anchor.test p Regex.Data.Anchor.eos = (p == s.endPos)
• Regex.Data.Anchor.test p Regex.Data.Anchor.wordBoundary = Regex.Data.String.isAtWordBoundary p
• Regex.Data.Anchor.test p Regex.Data.Anchor.nonWordBoundary = Regex.Data.String.isAtNonWordBoundary p