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
• star : Ast → Ast
• classes : Data.Classes → Ast
• perl : Data.PerlClass → Ast
• dot : Ast

instance Regex.Syntax.Parser.instInhabitedAst : Inhabited Ast

Equations

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

instance Regex.Syntax.Parser.instReprAst : Repr Ast

Equations

• Regex.Syntax.Parser.instReprAst = { reprPrec := Regex.Syntax.Parser.reprAst✝ }

instance Regex.Syntax.Parser.instDecidableEqAst : DecidableEq Ast

Equations

• Regex.Syntax.Parser.instDecidableEqAst = Regex.Syntax.Parser.decEqAst✝

def Regex.Syntax.Parser.Ast.toRegexAux (index : Nat) (ast : Ast) : Nat × Data.Expr

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.Parser.Ast.toRegexAux index Regex.Syntax.Parser.Ast.empty = (index, Regex.Data.Expr.empty)
• Regex.Syntax.Parser.Ast.toRegexAux index Regex.Syntax.Parser.Ast.epsilon = (index, Regex.Data.Expr.epsilon)
• Regex.Syntax.Parser.Ast.toRegexAux index (Regex.Syntax.Parser.Ast.anchor a) = (index, Regex.Data.Expr.anchor a)
• Regex.Syntax.Parser.Ast.toRegexAux index (Regex.Syntax.Parser.Ast.char a) = (index, Regex.Data.Expr.char a)
• Regex.Syntax.Parser.Ast.toRegexAux index a.group = match Regex.Syntax.Parser.Ast.toRegexAux (index + 1) a with | (index', r) => (index', Regex.Data.Expr.group index r)
• Regex.Syntax.Parser.Ast.toRegexAux index a.star = match Regex.Syntax.Parser.Ast.toRegexAux index a with | (index', r) => (index', r.star)
• Regex.Syntax.Parser.Ast.toRegexAux index (Regex.Syntax.Parser.Ast.classes a) = (index, Regex.Data.Expr.classes a)
• Regex.Syntax.Parser.Ast.toRegexAux index (Regex.Syntax.Parser.Ast.perl a) = (index, Regex.Data.Expr.classes { negated := false, classes := #[Regex.Data.Class.perl a] })

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

Equations

• ast.toRegex = (Regex.Syntax.Parser.Ast.toRegexAux 0 ast).snd