inductive Regex.Data.Anchor : Type

• start : Anchor
• eos : 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 }

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