inductive Regex.Data.Expr : Type

An inductive type that represents a regular expression.

• empty : Expr
• epsilon : Expr
• anchor : Anchor → Expr
• char : Char → Expr
• group : Nat → Expr → Expr
• alternate : Expr → Expr → Expr
• concat : Expr → Expr → Expr
• star : Bool → Expr → Expr
• classes : Classes → Expr

def Regex.Data.instReprExpr.repr : Expr → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Regex.Data.instReprExpr.repr Regex.Data.Expr.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.Data.Expr.empty")).group prec✝
• Regex.Data.instReprExpr.repr Regex.Data.Expr.epsilon prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.Data.Expr.epsilon")).group prec✝

instance Regex.Data.instReprExpr : Repr Expr

Equations

• Regex.Data.instReprExpr = { reprPrec := Regex.Data.instReprExpr.repr }

instance Regex.Data.instInhabitedExpr : Inhabited Expr

Equations

• Regex.Data.instInhabitedExpr = { default := Regex.Data.instInhabitedExpr.default }

def Regex.Data.instInhabitedExpr.default : Expr

Equations

• Regex.Data.instInhabitedExpr.default = Regex.Data.Expr.empty