@[reducible, inline]

abbrev Regex.Syntax.Parser.Combinators.Parser (s : 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 ε α = ((it : String.Iterator) → Regex.Syntax.Parser.Combinators.Result s it ε α)

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[inline]

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

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 : Bool} {ε α : Type} : Parser s ε α → Parser false ε α

Equations

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

@[inline]

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

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 : Bool} {ε α : Type} : Parser s ε α → Parser false ε (Option α)

Equations

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

@[inline]

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

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 : Bool} {ε α : Type} (expectedEof : ε) : Parser s ε α → Parser s ε α

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 : Bool} {ε α : Type} [ToString α] (name : String) (p : Parser s ε α) : Parser s ε α

Equations

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

@[inline]

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

Equations

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

@[inline]

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

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 : Bool} {ε α β : Type} (a : α) : Parser s ε β → Parser s ε α

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

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 : Bool} {ε α : Type} (p : Parser s ε α) (handle : ε → Parser s ε α) : Parser s ε α

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Regex.Syntax.Parser.Combinators.Parser.pure {ε α : Type} (a : α) : Parser 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 : Bool} {ε : Type} : Functor (Parser s ε)

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 : Bool} {ε : Type} : Seq (Parser s ε)

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 : Bool} {ε : Type} : SeqLeft (Parser s ε)

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 : Bool} {ε : Type} : SeqRight (Parser s ε)

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₁ s₂ : Bool} {ε α : Type} : HOrElse (Parser s₁ ε α) (Parser s₂ ε α) (Parser (s₁ && s₂) ε α)

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

instance Regex.Syntax.Parser.Combinators.Parser.instPureFalse {ε : Type} : Pure (Parser 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 {ε : Type} : Monad (Parser false ε)

Equations

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