def Regex.Syntax.Parser.Combinators.Rel.LE (it' it : String.Iterator) : Prop

Equations

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

def Regex.Syntax.Parser.Combinators.Rel.LT (it' it : String.Iterator) : Prop

Equations

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

def Regex.Syntax.Parser.Combinators.Rel (s : Bool) : String.Iterator → String.Iterator → Prop

Equations

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

instance Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLE : Trans LE LE LE

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLE = { trans := @Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLE._proof_1 }

instance Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLELT : Trans LE LT LT

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLELT = { trans := @Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLELT._proof_1 }

instance Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLTLE : Trans LT LE LT

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLTLE = { trans := @Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLTLE._proof_1 }

instance Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLT : Trans LT LT LT

Equations

• Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLT = { trans := @Regex.Syntax.Parser.Combinators.Rel.instTransIteratorLT._proof_1 }

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

Equations

• ⋯ = ⋯

def Regex.Syntax.Parser.Combinators.Rel.weaken {s : Bool} {it' it : String.Iterator} (rel : Rel s it' it) : Rel false it' it

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

def Regex.Syntax.Parser.Combinators.Rel.trans {s : Bool} {it it' it'' : String.Iterator} (h : Rel s it it') (h' : Rel s it' it'') : Rel s it it''

Equations

• ⋯ = ⋯

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

Equations

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

instance Regex.Syntax.Parser.Combinators.Rel.instTransIterator {s : Bool} : Trans (Rel s) (Rel s) (Rel s)

Equations

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