@[macro_inline]

def Regex.Syntax.Parser.Combinators.anyCharOrElse {s : String} {ε : Type} (unexpectedEof : ε) : Parser.LT s ε Char

Equations

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

@[macro_inline]

def Regex.Syntax.Parser.Combinators.testP {s : String} {ε : Type} (f : Char → Bool) : Parser.LE s ε Bool

Equations

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

@[macro_inline]

def Regex.Syntax.Parser.Combinators.test {s : String} {ε : Type} (c : Char) : Parser.LE s ε Bool

Equations

• Regex.Syntax.Parser.Combinators.test c = Regex.Syntax.Parser.Combinators.testP fun (x : Char) => decide (x = c)

@[macro_inline]

def Regex.Syntax.Parser.Combinators.charOrElse {s : String} {ε : Type} (c : Char) (unexpectedEof : ε) (unexpectedChar : Char → ε) : Parser.LT s ε Char

Equations

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

@[irreducible]

def Regex.Syntax.Parser.Combinators.foldlAux {s : String} {ε α β : Type} (init : β) (f : β → α → β) (p : Parser.LT s ε α) (pos : s.ValidPos) : Result.LE pos ε β

Equations

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

def Regex.Syntax.Parser.Combinators.foldl {s : String} {ε α β : Type} (init : β) (f : β → α → β) (p : Parser.LT s ε α) : Parser.LE s ε β

Equations

• Regex.Syntax.Parser.Combinators.foldl init f p = Regex.Syntax.Parser.Combinators.foldlAux init f p

@[inline]

def Regex.Syntax.Parser.Combinators.foldl1 {s : String} {ε α : Type} (f : α → α → α) (p : Parser.LT s ε α) : Parser.LT s ε α

Equations

• Regex.Syntax.Parser.Combinators.foldl1 f p = Regex.Syntax.Parser.Combinators.Parser.bindOr p fun (a : α) => Regex.Syntax.Parser.Combinators.foldl a f p

@[inline]

def Regex.Syntax.Parser.Combinators.many1 {s : String} {ε α : Type} (p : Parser.LT s ε α) : Parser.LT s ε (Array α)

Equations

• Regex.Syntax.Parser.Combinators.many1 p = Regex.Syntax.Parser.Combinators.Parser.bindOr p fun (a : α) => Regex.Syntax.Parser.Combinators.foldl #[a] (fun (acc : Array α) (a : α) => acc.push a) p

@[inline]

def Regex.Syntax.Parser.Combinators.betweenOr {s : String} {strict₁ strict₂ strict₃ : Bool} {ε α β γ : Type} (l : Parser s strict₁ ε α) (r : Parser s strict₃ ε γ) (m : Parser s strict₂ ε β) : Parser s (strict₁ || strict₂ || strict₃) ε β

Equations

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

def Regex.Syntax.Parser.Combinators.foldlNAux {s : String} {strict : Bool} {ε α β : Type} (init : β) (f : β → α → β) (p : Parser s strict ε α) (n : Nat) (pos : s.ValidPos) : Result (decide (n ≠ 0) && strict) pos ε β

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.Parser.Combinators.foldlNAux init f p 0 pos = Regex.Syntax.Parser.Combinators.Result.imp ⋯ (Regex.Syntax.Parser.Combinators.Result.pure init)

@[inline]

def Regex.Syntax.Parser.Combinators.foldlN {s : String} {strict : Bool} {ε α β : Type} (init : β) (f : β → α → β) (p : Parser s strict ε α) (n : Nat) : Parser s (decide (n ≠ 0) && strict) ε β

Equations

• Regex.Syntax.Parser.Combinators.foldlN init f p n x✝ = Regex.Syntax.Parser.Combinators.foldlNAux init f p n x✝

@[inline]

def Regex.Syntax.Parser.Combinators.foldlPos {s : String} {ε α β : Type} (init : β) (f : β → α → β) (p : Parser.LT s ε α) (n : Nat) [NeZero n] : Parser.LT s ε β

Equations

• Regex.Syntax.Parser.Combinators.foldlPos init f p n = Regex.Syntax.Parser.Combinators.Parser.cast ⋯ (Regex.Syntax.Parser.Combinators.foldlN init f p n)