@[macro_inline]

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

Equations

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

@[macro_inline]

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

Equations

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

@[macro_inline]

def Regex.Syntax.Parser.Combinators.test {ε : Type} (c : Char) : Parser.LE ε 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 {ε : Type} (c : Char) (unexpectedEof : ε) (unexpectedChar : Char → ε) : Parser.LT ε Char

Equations

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

@[irreducible]

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

Equations

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

@[inline]

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

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 {ε α : Type} (p : Parser.LT ε α) : Parser.LT ε (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₁ s₂ s₃ : Bool} {ε α β γ : Type} (l : Parser s₁ ε α) (r : Parser s₃ ε γ) (m : Parser s₂ ε β) : Parser (s₁ || s₂ || s₃) ε β

Equations

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

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

Equations

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

@[inline]

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

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 {ε α β : Type} (init : β) (f : β → α → β) (p : Parser.LT ε α) (n : Nat) [NeZero n] : Parser.LT ε β

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)