@[reducible, inline]

abbrev Regex.Syntax.Parser.Combinators.Parser (s : String) (strict : Bool) (ε α : Type) : Type

Total parser combinators a la idris2-parser.

s controls whether the input is strictly decreasing.

Equations

• Regex.Syntax.Parser.Combinators.Parser s strict ε α = ((p : s.ValidPos) → Regex.Syntax.Parser.Combinators.Result strict p ε α)

@[reducible, inline]

abbrev Regex.Syntax.Parser.Combinators.Parser.LE (s : String) (ε α : Type) : Type

Equations

• Regex.Syntax.Parser.Combinators.Parser.LE s ε α = Regex.Syntax.Parser.Combinators.Parser s false ε α

@[reducible, inline]

abbrev Regex.Syntax.Parser.Combinators.Parser.LT (s : String) (ε α : Type) : Type

Equations

• Regex.Syntax.Parser.Combinators.Parser.LT s ε α = Regex.Syntax.Parser.Combinators.Parser s true ε α

@[inline]

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

Equations

• Regex.Syntax.Parser.Combinators.Parser.imp h x✝¹ x✝ = Regex.Syntax.Parser.Combinators.Result.imp h (x✝¹ x✝)

@[inline]

def Regex.Syntax.Parser.Combinators.Parser.weaken {s : String} {strict : Bool} {ε α : Type} : Parser s strict ε α → Parser s false ε α

Equations

• x✝¹.weaken x✝ = (x✝¹ x✝).weaken

@[inline]

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

Equations

• Regex.Syntax.Parser.Combinators.Parser.cast h x✝¹ x✝ = Regex.Syntax.Parser.Combinators.Result.cast h (x✝¹ x✝)

@[inline]

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

Equations

• x✝¹.opt x✝ = (x✝¹ x✝).opt

@[inline]

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

Equations

• Regex.Syntax.Parser.Combinators.Parser.guard f x✝¹ x✝ = Regex.Syntax.Parser.Combinators.Result.guard f (x✝¹ x✝)

@[inline]

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

Equations

• Regex.Syntax.Parser.Combinators.Parser.complete expectedEof x✝¹ x✝ = Regex.Syntax.Parser.Combinators.Result.complete expectedEof (x✝¹ x✝)

@[inline]

def Regex.Syntax.Parser.Combinators.Parser.debug {s : String} {strict : Bool} {ε α : Type} [ToString α] (name : String) (p : Parser s strict ε α) : Parser s strict ε α

Equations

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

@[inline]

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

Equations

• x✝¹.commit x✝ = (x✝¹ x✝).commit

@[inline]

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

Equations

• Regex.Syntax.Parser.Combinators.Parser.map f x✝¹ x✝ = Regex.Syntax.Parser.Combinators.Result.map f (x✝¹ x✝)

@[inline]

def Regex.Syntax.Parser.Combinators.Parser.mapConst {s : String} {strict : Bool} {ε α β : Type} (a : α) : Parser s strict ε β → Parser s strict ε α

Equations

• Regex.Syntax.Parser.Combinators.Parser.mapConst a x✝¹ x✝ = Functor.mapConst a (x✝¹ x✝)

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Regex.Syntax.Parser.Combinators.Parser.bindOr {s : String} {strict₁ strict₂ : Bool} {ε α β : Type} (p : Parser s strict₁ ε α) (f : α → Parser s strict₂ ε β) : Parser s (strict₁ || strict₂) ε β

Equations

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

@[inline]

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

Equations

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

@[inline]

def Regex.Syntax.Parser.Combinators.Parser.pure {s : String} {ε α : Type} (a : α) : Parser s false ε α

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

instance Regex.Syntax.Parser.Combinators.Parser.instPureFalse {s : String} {ε : Type} : Pure (Parser s false ε)

Equations

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

@[inline]

instance Regex.Syntax.Parser.Combinators.Parser.instMonadFalse {s : String} {ε : Type} : Monad (Parser s false ε)

Equations

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