inductive Regex.Syntax.Parser.Ast : Type

• empty : Ast
• epsilon : Ast
• anchor : Data.Anchor → Ast
• char : Char → Ast
• group : Ast → Ast
• alternate : Ast → Ast → Ast
• concat : Ast → Ast → Ast
• repeat : Nat → Option Nat → Bool → Ast → Ast
• classes : Data.Classes → Ast
• perl : Data.PerlClass → Ast
• dot : Ast
• flags (caseInsensitive : Bool) : Ast

instance Regex.Syntax.Parser.instInhabitedAst : Inhabited Ast

Equations

• Regex.Syntax.Parser.instInhabitedAst = { default := Regex.Syntax.Parser.instInhabitedAst.default }

def Regex.Syntax.Parser.instInhabitedAst.default : Ast

Equations

• Regex.Syntax.Parser.instInhabitedAst.default = Regex.Syntax.Parser.Ast.empty

def Regex.Syntax.Parser.instReprAst.repr : Ast → Nat → Std.Format

Equations

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

instance Regex.Syntax.Parser.instReprAst : Repr Ast

Equations

• Regex.Syntax.Parser.instReprAst = { reprPrec := Regex.Syntax.Parser.instReprAst.repr }

instance Regex.Syntax.Parser.instDecidableEqAst : DecidableEq Ast

Equations

• Regex.Syntax.Parser.instDecidableEqAst = Regex.Syntax.Parser.instDecidableEqAst.decEq

def Regex.Syntax.Parser.instDecidableEqAst.decEq (x✝ x✝¹ : Ast) : Decidable (x✝ = x✝¹)

Equations

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

def Regex.Syntax.Parser.repeatConcat (e : Data.Expr) (n : Nat) : Data.Expr

Equations

• Regex.Syntax.Parser.repeatConcat e n = Regex.Syntax.Parser.repeatConcat.go✝ e e (n - 1)

def Regex.Syntax.Parser.applyRepetitions (min : Nat) (max : Option Nat) (greedy : Bool) (e : Data.Expr) : Data.Expr

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.Parser.applyRepetitions 0 (some 1) greedy e = if greedy = true then e.alternate Regex.Data.Expr.epsilon else Regex.Data.Expr.epsilon.alternate e
• Regex.Syntax.Parser.applyRepetitions 0 none greedy e = Regex.Data.Expr.star greedy e
• Regex.Syntax.Parser.applyRepetitions 1 none greedy e = e.concat (Regex.Data.Expr.star greedy e)
• Regex.Syntax.Parser.applyRepetitions min none greedy e = (Regex.Syntax.Parser.repeatConcat e min).concat (Regex.Data.Expr.star greedy e)

def Regex.Syntax.Parser.charToCaseInsensitive (c : Char) : Data.Expr

Equations

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

structure Regex.Syntax.Parser.ToRegexState : Type

• index : Nat
• caseInsensitive : Bool

def Regex.Syntax.Parser.Ast.toRegexAux (state : ToRegexState) (ast : Ast) : ToRegexState × Data.Expr

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.Parser.Ast.toRegexAux state Regex.Syntax.Parser.Ast.empty = (state, Regex.Data.Expr.empty)
• Regex.Syntax.Parser.Ast.toRegexAux state Regex.Syntax.Parser.Ast.epsilon = (state, Regex.Data.Expr.epsilon)
• Regex.Syntax.Parser.Ast.toRegexAux state (Regex.Syntax.Parser.Ast.anchor a) = (state, Regex.Data.Expr.anchor a)
• Regex.Syntax.Parser.Ast.toRegexAux state (Regex.Syntax.Parser.Ast.classes a) = (state, Regex.Data.Expr.classes a)
• Regex.Syntax.Parser.Ast.toRegexAux state (Regex.Syntax.Parser.Ast.perl a) = (state, Regex.Data.Expr.classes (Regex.Data.Classes.atom (Regex.Data.Class.perl a)))
• Regex.Syntax.Parser.Ast.toRegexAux state (Regex.Syntax.Parser.Ast.flags a) = ({ index := state.index, caseInsensitive := a }, Regex.Data.Expr.epsilon)

def Regex.Syntax.Parser.Ast.toRegex (ast : Ast) : Data.Expr

Equations

• ast.toRegex = (Regex.Syntax.Parser.Ast.toRegexAux { index := 0 } ast).snd