inductive Regex.Syntax.Parser.Combinators.Result {s : String} (strict : Bool) (p : s.ValidPos) (ε α : Type) : Type

• ok {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} : α → (p' : s.ValidPos) → Rel strict p' p → Result strict p ε α
• error {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} : ε → Result strict p ε α
• fatal {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} : ε → Result strict p ε α

@[reducible, inline]

abbrev Regex.Syntax.Parser.Combinators.Result.LE {s : String} (p : s.ValidPos) (ε α : Type) : Type

Equations

• Regex.Syntax.Parser.Combinators.Result.LE p ε α = Regex.Syntax.Parser.Combinators.Result false p ε α

@[reducible, inline]

abbrev Regex.Syntax.Parser.Combinators.Result.LT {s : String} (p : s.ValidPos) (ε α : Type) : Type

Equations

• Regex.Syntax.Parser.Combinators.Result.LT p ε α = Regex.Syntax.Parser.Combinators.Result true p ε α

@[inline]

def Regex.Syntax.Parser.Combinators.Result.imp {s : String} {strict₁ strict₂ : Bool} {p : s.ValidPos} {ε α : Type} (h : strict₂ = true → strict₁ = true) : Result strict₁ p ε α → Result strict₂ p ε α

Equations

• Regex.Syntax.Parser.Combinators.Result.imp h (Regex.Syntax.Parser.Combinators.Result.ok a pos' h') = Regex.Syntax.Parser.Combinators.Result.ok a pos' ⋯
• Regex.Syntax.Parser.Combinators.Result.imp h (Regex.Syntax.Parser.Combinators.Result.error e) = Regex.Syntax.Parser.Combinators.Result.error e
• Regex.Syntax.Parser.Combinators.Result.imp h (Regex.Syntax.Parser.Combinators.Result.fatal e) = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

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

Equations

• Regex.Syntax.Parser.Combinators.Result.transOr h (Regex.Syntax.Parser.Combinators.Result.ok a pos' h') = Regex.Syntax.Parser.Combinators.Result.ok a pos' ⋯
• Regex.Syntax.Parser.Combinators.Result.transOr h (Regex.Syntax.Parser.Combinators.Result.error e) = Regex.Syntax.Parser.Combinators.Result.error e
• Regex.Syntax.Parser.Combinators.Result.transOr h (Regex.Syntax.Parser.Combinators.Result.fatal e) = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

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

Equations

• Regex.Syntax.Parser.Combinators.Result.trans h (Regex.Syntax.Parser.Combinators.Result.ok a pos' h') = Regex.Syntax.Parser.Combinators.Result.ok a pos' ⋯
• Regex.Syntax.Parser.Combinators.Result.trans h (Regex.Syntax.Parser.Combinators.Result.error e) = Regex.Syntax.Parser.Combinators.Result.error e
• Regex.Syntax.Parser.Combinators.Result.trans h (Regex.Syntax.Parser.Combinators.Result.fatal e) = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.cast {s : String} {strict₁ strict₂ : Bool} {p : s.ValidPos} {ε α : Type} (h : strict₁ = strict₂) (res : Result strict₁ p ε α) : Result strict₂ p ε α

Equations

• Regex.Syntax.Parser.Combinators.Result.cast h res = Regex.Syntax.Parser.Combinators.Result.imp ⋯ res

@[inline]

def Regex.Syntax.Parser.Combinators.Result.weaken {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} (res : Result strict p ε α) : Result false p ε α

Equations

• res.weaken = Regex.Syntax.Parser.Combinators.Result.imp ⋯ res

@[inline]

def Regex.Syntax.Parser.Combinators.Result.toExcept {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} (res : Result strict p ε α) : Except ε α

Equations

• (Regex.Syntax.Parser.Combinators.Result.ok a pos' h').toExcept = Except.ok a
• (Regex.Syntax.Parser.Combinators.Result.error e).toExcept = Except.error e
• (Regex.Syntax.Parser.Combinators.Result.fatal e).toExcept = Except.error e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.opt {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} : Result strict p ε α → Result false p ε (Option α)

Equations

• (Regex.Syntax.Parser.Combinators.Result.ok a pos' h').opt = Regex.Syntax.Parser.Combinators.Result.ok (some a) pos' ⋯
• (Regex.Syntax.Parser.Combinators.Result.error e).opt = Regex.Syntax.Parser.Combinators.Result.ok none p ⋯
• (Regex.Syntax.Parser.Combinators.Result.fatal e).opt = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.complete {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} (expectedEof : ε) : Result strict p ε α → Result strict p ε α

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.Parser.Combinators.Result.complete expectedEof (Regex.Syntax.Parser.Combinators.Result.error e) = Regex.Syntax.Parser.Combinators.Result.error e
• Regex.Syntax.Parser.Combinators.Result.complete expectedEof (Regex.Syntax.Parser.Combinators.Result.fatal e) = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.commit {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} : Result strict p ε α → Result strict p ε α

Equations

• (Regex.Syntax.Parser.Combinators.Result.ok a pos' h').commit = Regex.Syntax.Parser.Combinators.Result.ok a pos' h'
• (Regex.Syntax.Parser.Combinators.Result.error e).commit = Regex.Syntax.Parser.Combinators.Result.fatal e
• (Regex.Syntax.Parser.Combinators.Result.fatal e).commit = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.guard {s : String} {strict : Bool} {p : s.ValidPos} {ε α β : Type} (f : α → Except ε β) : Result strict p ε α → Result strict p ε β

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.Parser.Combinators.Result.guard f (Regex.Syntax.Parser.Combinators.Result.error e) = Regex.Syntax.Parser.Combinators.Result.error e
• Regex.Syntax.Parser.Combinators.Result.guard f (Regex.Syntax.Parser.Combinators.Result.fatal e) = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.map' {s : String} {strict : Bool} {p : s.ValidPos} {ε α β : Type} (f : α → (p' : s.ValidPos) → Rel strict p' p → β) : Result strict p ε α → Result strict p ε β

Equations

• Regex.Syntax.Parser.Combinators.Result.map' f (Regex.Syntax.Parser.Combinators.Result.ok a pos' h') = Regex.Syntax.Parser.Combinators.Result.ok (f a pos' h') pos' h'
• Regex.Syntax.Parser.Combinators.Result.map' f (Regex.Syntax.Parser.Combinators.Result.error e) = Regex.Syntax.Parser.Combinators.Result.error e
• Regex.Syntax.Parser.Combinators.Result.map' f (Regex.Syntax.Parser.Combinators.Result.fatal e) = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.map {s : String} {strict : Bool} {p : s.ValidPos} {ε α β : Type} (f : α → β) : Result strict p ε α → Result strict p ε β

Equations

• Regex.Syntax.Parser.Combinators.Result.map f = Regex.Syntax.Parser.Combinators.Result.map' fun (a : α) (x : s.ValidPos) (x_1 : Regex.Syntax.Parser.Combinators.Rel strict x p) => f a

@[inline]

def Regex.Syntax.Parser.Combinators.Result.seq {s : String} {strict : Bool} {p : s.ValidPos} {ε α β : Type} (mf : Result strict p ε (α → β)) (mx : Unit → Result strict p ε α) : Result strict p ε β

Equations

• One or more equations did not get rendered due to their size.
• (Regex.Syntax.Parser.Combinators.Result.error e).seq mx = Regex.Syntax.Parser.Combinators.Result.error e
• (Regex.Syntax.Parser.Combinators.Result.fatal e).seq mx = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.seqLeft {s : String} {strict : Bool} {p : s.ValidPos} {ε α β : Type} (mx : Result strict p ε α) (my : Unit → Result strict p ε β) : Result strict p ε α

Equations

• One or more equations did not get rendered due to their size.
• (Regex.Syntax.Parser.Combinators.Result.error e).seqLeft my = Regex.Syntax.Parser.Combinators.Result.error e
• (Regex.Syntax.Parser.Combinators.Result.fatal e).seqLeft my = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.seqRight {s : String} {strict : Bool} {p : s.ValidPos} {ε α β : Type} (mx : Result strict p ε α) (my : Unit → Result strict p ε β) : Result strict p ε β

Equations

• One or more equations did not get rendered due to their size.
• (Regex.Syntax.Parser.Combinators.Result.error e).seqRight my = Regex.Syntax.Parser.Combinators.Result.error e
• (Regex.Syntax.Parser.Combinators.Result.fatal e).seqRight my = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.hOrElse {s : String} {strict₁ strict₂ : Bool} {p : s.ValidPos} {ε α : Type} (mx : Result strict₁ p ε α) (my : Unit → Result strict₂ p ε α) : Result (strict₁ && strict₂) p ε α

Equations

• (Regex.Syntax.Parser.Combinators.Result.ok a pos' h').hOrElse my = Regex.Syntax.Parser.Combinators.Result.ok a pos' ⋯
• (Regex.Syntax.Parser.Combinators.Result.error e).hOrElse my = Regex.Syntax.Parser.Combinators.Result.imp ⋯ (my ())
• (Regex.Syntax.Parser.Combinators.Result.fatal e).hOrElse my = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.orElse {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} : Result strict p ε α → (Unit → Result strict p ε α) → Result strict p ε α

Equations

• (Regex.Syntax.Parser.Combinators.Result.ok a p' h).orElse x✝ = Regex.Syntax.Parser.Combinators.Result.ok a p' h
• (Regex.Syntax.Parser.Combinators.Result.error a).orElse x✝ = x✝ ()
• (Regex.Syntax.Parser.Combinators.Result.fatal e).orElse x✝ = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.throw {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} (e : ε) : Result strict p ε α

Equations

• Regex.Syntax.Parser.Combinators.Result.throw e = Regex.Syntax.Parser.Combinators.Result.error e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.tryCatch {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} (mx : Result strict p ε α) (handle : ε → Result strict p ε α) : Result strict p ε α

Equations

• (Regex.Syntax.Parser.Combinators.Result.ok a pos' h').tryCatch handle = Regex.Syntax.Parser.Combinators.Result.ok a pos' h'
• (Regex.Syntax.Parser.Combinators.Result.error e).tryCatch handle = handle e
• (Regex.Syntax.Parser.Combinators.Result.fatal e).tryCatch handle = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.bind' {s : String} {strict₁ strict₂ : Bool} {p : s.ValidPos} {ε α β : Type} (mx : Result strict₁ p ε α) (f : α → (p' : s.ValidPos) → Rel strict₁ p' p → Result strict₂ p' ε β) : Result (strict₁ || strict₂) p ε β

Equations

• (Regex.Syntax.Parser.Combinators.Result.ok a pos' h').bind' f = Regex.Syntax.Parser.Combinators.Result.cast ⋯ (Regex.Syntax.Parser.Combinators.Result.transOr h' (f a pos' h'))
• (Regex.Syntax.Parser.Combinators.Result.error e).bind' f = Regex.Syntax.Parser.Combinators.Result.error e
• (Regex.Syntax.Parser.Combinators.Result.fatal e).bind' f = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.bind {s : String} {strict : Bool} {p : s.ValidPos} {ε α β : Type} (mx : Result strict p ε α) (f : α → Result strict p ε β) : Result strict p ε β

Equations

• (Regex.Syntax.Parser.Combinators.Result.ok a pos' h').bind f = f a
• (Regex.Syntax.Parser.Combinators.Result.error e).bind f = Regex.Syntax.Parser.Combinators.Result.error e
• (Regex.Syntax.Parser.Combinators.Result.fatal e).bind f = Regex.Syntax.Parser.Combinators.Result.fatal e

@[inline]

def Regex.Syntax.Parser.Combinators.Result.pure {s : String} {p : s.ValidPos} {ε α : Type} (a : α) : LE p ε α

Equations

• Regex.Syntax.Parser.Combinators.Result.pure a = Regex.Syntax.Parser.Combinators.Result.ok a p ⋯

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instFunctor {s : String} {strict : Bool} {p : s.ValidPos} {ε : Type} : Functor (Result strict p ε)

Equations

• Regex.Syntax.Parser.Combinators.Result.instFunctor = { map := fun {α β : Type} => Regex.Syntax.Parser.Combinators.Result.map }

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instSeq {s : String} {strict : Bool} {p : s.ValidPos} {ε : Type} : Seq (Result strict p ε)

Equations

• Regex.Syntax.Parser.Combinators.Result.instSeq = { seq := fun {α β : Type} => Regex.Syntax.Parser.Combinators.Result.seq }

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instSeqLeft {s : String} {strict : Bool} {p : s.ValidPos} {ε : Type} : SeqLeft (Result strict p ε)

Equations

• Regex.Syntax.Parser.Combinators.Result.instSeqLeft = { seqLeft := fun {α β : Type} => Regex.Syntax.Parser.Combinators.Result.seqLeft }

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instSeqRight {s : String} {strict : Bool} {p : s.ValidPos} {ε : Type} : SeqRight (Result strict p ε)

Equations

• Regex.Syntax.Parser.Combinators.Result.instSeqRight = { seqRight := fun {α β : Type} => Regex.Syntax.Parser.Combinators.Result.seqRight }

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instHOrElseAnd {s : String} {strict₁ strict₂ : Bool} {p : s.ValidPos} {ε α : Type} : HOrElse (Result strict₁ p ε α) (Result strict₂ p ε α) (Result (strict₁ && strict₂) p ε α)

Equations

• Regex.Syntax.Parser.Combinators.Result.instHOrElseAnd = { hOrElse := Regex.Syntax.Parser.Combinators.Result.hOrElse }

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instOrElse {s : String} {strict : Bool} {p : s.ValidPos} {ε α : Type} : OrElse (Result strict p ε α)

Equations

• Regex.Syntax.Parser.Combinators.Result.instOrElse = { orElse := Regex.Syntax.Parser.Combinators.Result.orElse }

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instMonadExceptOf {s : String} {strict : Bool} {p : s.ValidPos} {ε : Type} : MonadExceptOf ε (Result strict p ε)

Equations

• One or more equations did not get rendered due to their size.

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instBind {s : String} {strict : Bool} {p : s.ValidPos} {ε : Type} : Bind (Result strict p ε)

Equations

• Regex.Syntax.Parser.Combinators.Result.instBind = { bind := fun {α β : Type} => Regex.Syntax.Parser.Combinators.Result.bind }

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instPureLE {s : String} {p : s.ValidPos} {ε : Type} : Pure (LE p ε)

Equations

• Regex.Syntax.Parser.Combinators.Result.instPureLE = { pure := fun {α : Type} => Regex.Syntax.Parser.Combinators.Result.pure }

@[inline]

instance Regex.Syntax.Parser.Combinators.Result.instMonadLE {s : String} {p : s.ValidPos} {ε : Type} : Monad (LE p ε)

Equations

• One or more equations did not get rendered due to their size.