def Regex.Syntax.Parser.Combinators.Rel.LE {s : String} (p' p : s.ValidPos) : Prop

Equations

• Regex.Syntax.Parser.Combinators.Rel.LE p' p = (p ≤ p')

def Regex.Syntax.Parser.Combinators.Rel.LT {s : String} (p' p : s.ValidPos) : Prop

Equations

• Regex.Syntax.Parser.Combinators.Rel.LT p' p = (p < p')

def Regex.Syntax.Parser.Combinators.Rel {s : String} (strict : Bool) : s.ValidPos → s.ValidPos → Prop

Equations

• Regex.Syntax.Parser.Combinators.Rel strict = if strict = true then Regex.Syntax.Parser.Combinators.Rel.LT else Regex.Syntax.Parser.Combinators.Rel.LE

instance Regex.Syntax.Parser.Combinators.Rel.instTransValidPosLE {s : String} : Trans LE LE LE

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransValidPosLE = { trans := ⋯ }

instance Regex.Syntax.Parser.Combinators.Rel.instTransValidPosLELT {s : String} : Trans LE LT LT

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransValidPosLELT = { trans := ⋯ }

instance Regex.Syntax.Parser.Combinators.Rel.instTransValidPosLTLE {s : String} : Trans LT LE LT

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransValidPosLTLE = { trans := ⋯ }

instance Regex.Syntax.Parser.Combinators.Rel.instTransValidPosLT {s : String} : Trans LT LT LT

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransValidPosLT = { trans := ⋯ }

def Regex.Syntax.Parser.Combinators.Rel.imp {s : String} {strict₁ strict₂ : Bool} {p' p : s.ValidPos} (h : strict₂ = true → strict₁ = true) (rel : Rel strict₁ p' p) : Rel strict₂ p' p

Equations

• ⋯ = ⋯

def Regex.Syntax.Parser.Combinators.Rel.weaken {s : String} {strict : Bool} {p' p : s.ValidPos} (rel : Rel strict p' p) : Rel false p' p

Equations

• ⋯ = ⋯

def Regex.Syntax.Parser.Combinators.Rel.transOr {s : String} {strict₁ strict₂ : Bool} {p p' p'' : s.ValidPos} (h : Rel strict₁ p p') (h' : Rel strict₂ p' p'') : Rel (strict₁ || strict₂) p p''

Equations

• ⋯ = ⋯

def Regex.Syntax.Parser.Combinators.Rel.trans {s : String} {strict : Bool} {p p' p'' : s.ValidPos} (h : Rel strict p p') (h' : Rel strict p' p'') : Rel strict p p''

Equations

• ⋯ = ⋯

instance Regex.Syntax.Parser.Combinators.Rel.instTransValidPosOr {s : String} {strict₁ strict₂ : Bool} : Trans (Rel strict₁) (Rel strict₂) (Rel (strict₁ || strict₂))

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransValidPosOr = { trans := ⋯ }

instance Regex.Syntax.Parser.Combinators.Rel.instTransValidPos {s : String} {strict : Bool} : Trans (Rel strict) (Rel strict) (Rel strict)

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransValidPos = { trans := ⋯ }