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

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