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 → 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.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.repeatConcat.go (e accum : Data.Expr) : Nat → Data.Expr

Equations

• Regex.Syntax.Parser.repeatConcat.go e accum 0 = accum
• Regex.Syntax.Parser.repeatConcat.go e accum n.succ = Regex.Syntax.Parser.repeatConcat.go e (accum.concat e) n

def Regex.Syntax.Parser.applyRepetitions (min : Nat) (max : Option Nat) (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) e = e.alternate Regex.Data.Expr.epsilon
• Regex.Syntax.Parser.applyRepetitions 0 none e = e.star
• Regex.Syntax.Parser.applyRepetitions 1 none e = e.concat e.star
• Regex.Syntax.Parser.applyRepetitions min none e = (Regex.Syntax.Parser.repeatConcat e min).concat e.star
• Regex.Syntax.Parser.applyRepetitions 0 (some max_2) e = if (max_2 == 0) = true then Regex.Data.Expr.epsilon else Regex.Syntax.Parser.repeatConcat (e.alternate Regex.Data.Expr.epsilon) max_2

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 (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