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

Equations

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

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

Equations

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

def Regex.Syntax.Parser.Combinators.Rel {s : String} (strict : Bool) : s.Pos → s.Pos → 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_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

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

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

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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