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 : Expr → Expr
• classes : Classes → Expr

instance Regex.Data.instReprExpr : Repr Expr

Equations

• Regex.Data.instReprExpr = { reprPrec := Regex.Data.reprExpr✝ }

instance Regex.Data.instInhabitedExpr : Inhabited Expr

Equations

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