inductive Regex.Data.PerlClassKind : Type

• digit : PerlClassKind
• space : PerlClassKind
• word : PerlClassKind

instance Regex.Data.instReprPerlClassKind : Repr PerlClassKind

Equations

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

def Regex.Data.instReprPerlClassKind.repr : PerlClassKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Regex.Data.instDecidableEqPerlClassKind : DecidableEq PerlClassKind

Equations

• Regex.Data.instDecidableEqPerlClassKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Regex.Data.instInhabitedPerlClassKind : Inhabited PerlClassKind

Equations

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

def Regex.Data.instInhabitedPerlClassKind.default : PerlClassKind

Equations

• Regex.Data.instInhabitedPerlClassKind.default = Regex.Data.PerlClassKind.digit

def Regex.Data.instToExprPerlClassKind.toExpr : PerlClassKind → Lean.Expr

Equations

• Regex.Data.instToExprPerlClassKind.toExpr Regex.Data.PerlClassKind.digit = Lean.Expr.const `Regex.Data.PerlClassKind.digit []
• Regex.Data.instToExprPerlClassKind.toExpr Regex.Data.PerlClassKind.space = Lean.Expr.const `Regex.Data.PerlClassKind.space []
• Regex.Data.instToExprPerlClassKind.toExpr Regex.Data.PerlClassKind.word = Lean.Expr.const `Regex.Data.PerlClassKind.word []

instance Regex.Data.instToExprPerlClassKind : Lean.ToExpr PerlClassKind

Equations

• Regex.Data.instToExprPerlClassKind = { toExpr := Regex.Data.instToExprPerlClassKind.toExpr, toTypeExpr := Lean.Expr.const `Regex.Data.PerlClassKind [] }

def Regex.Data.PerlClassKind.mem (c : Char) (kind : PerlClassKind) : Bool

Equations

• Regex.Data.PerlClassKind.mem c Regex.Data.PerlClassKind.digit = c.isDigit
• Regex.Data.PerlClassKind.mem c Regex.Data.PerlClassKind.space = (c == ' ' || c == '\t' || c == '\n' || c == '\x0d' || c == '\x0c')
• Regex.Data.PerlClassKind.mem c Regex.Data.PerlClassKind.word = (c.isAlphanum || c == '_')

structure Regex.Data.PerlClass : Type

• negated : Bool
• kind : PerlClassKind

def Regex.Data.instReprPerlClass.repr : PerlClass → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Regex.Data.instReprPerlClass : Repr PerlClass

Equations

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

instance Regex.Data.instDecidableEqPerlClass : DecidableEq PerlClass

Equations

• Regex.Data.instDecidableEqPerlClass = Regex.Data.instDecidableEqPerlClass.decEq

def Regex.Data.instDecidableEqPerlClass.decEq (x✝ x✝¹ : PerlClass) : Decidable (x✝ = x✝¹)

Equations

• Regex.Data.instDecidableEqPerlClass.decEq { negated := a, kind := a_1 } { negated := b, kind := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Regex.Data.instInhabitedPerlClass : Inhabited PerlClass

Equations

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

def Regex.Data.instInhabitedPerlClass.default : PerlClass

Equations

• Regex.Data.instInhabitedPerlClass.default = { negated := default, kind := default }

def Regex.Data.instToExprPerlClass.toExpr : PerlClass → Lean.Expr

Equations

• Regex.Data.instToExprPerlClass.toExpr { negated := a, kind := a_1 } = ((Lean.Expr.const `Regex.Data.PerlClass.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

instance Regex.Data.instToExprPerlClass : Lean.ToExpr PerlClass

Equations

• Regex.Data.instToExprPerlClass = { toExpr := Regex.Data.instToExprPerlClass.toExpr, toTypeExpr := Lean.Expr.const `Regex.Data.PerlClass [] }

def Regex.Data.PerlClass.mem (c : Char) (pc : PerlClass) : Bool

Equations

• Regex.Data.PerlClass.mem c pc = if pc.negated = true then !Regex.Data.PerlClassKind.mem c pc.kind else Regex.Data.PerlClassKind.mem c pc.kind

inductive Regex.Data.Class : Type

• single : Char → Class
• range (s e : Char) : Class
• perl : PerlClass → Class

instance Regex.Data.instReprClass : Repr Class

Equations

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

def Regex.Data.instReprClass.repr : Class → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Regex.Data.instDecidableEqClass.decEq (x✝ x✝¹ : Class) : Decidable (x✝ = x✝¹)

Equations

• Regex.Data.instDecidableEqClass.decEq (Regex.Data.Class.single a) (Regex.Data.Class.single b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Regex.Data.instDecidableEqClass.decEq (Regex.Data.Class.single a) (Regex.Data.Class.range s e) = isFalse ⋯
• Regex.Data.instDecidableEqClass.decEq (Regex.Data.Class.single a) (Regex.Data.Class.perl a_1) = isFalse ⋯
• Regex.Data.instDecidableEqClass.decEq (Regex.Data.Class.range s e) (Regex.Data.Class.single a) = isFalse ⋯
• Regex.Data.instDecidableEqClass.decEq (Regex.Data.Class.range a a_1) (Regex.Data.Class.range b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Regex.Data.instDecidableEqClass.decEq (Regex.Data.Class.range s e) (Regex.Data.Class.perl a) = isFalse ⋯
• Regex.Data.instDecidableEqClass.decEq (Regex.Data.Class.perl a) (Regex.Data.Class.single a_1) = isFalse ⋯
• Regex.Data.instDecidableEqClass.decEq (Regex.Data.Class.perl a) (Regex.Data.Class.range s e) = isFalse ⋯
• Regex.Data.instDecidableEqClass.decEq (Regex.Data.Class.perl a) (Regex.Data.Class.perl b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Regex.Data.instDecidableEqClass : DecidableEq Class

Equations

• Regex.Data.instDecidableEqClass = Regex.Data.instDecidableEqClass.decEq

def Regex.Data.instInhabitedClass.default : Class

Equations

• Regex.Data.instInhabitedClass.default = Regex.Data.Class.single default

instance Regex.Data.instInhabitedClass : Inhabited Class

Equations

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

def Regex.Data.instToExprClass.toExpr : Class → Lean.Expr

Equations

• Regex.Data.instToExprClass.toExpr (Regex.Data.Class.single a) = (Lean.Expr.const `Regex.Data.Class.single []).app (Lean.toExpr a)
• Regex.Data.instToExprClass.toExpr (Regex.Data.Class.range a a_1) = ((Lean.Expr.const `Regex.Data.Class.range []).app (Lean.toExpr a)).app (Lean.toExpr a_1)
• Regex.Data.instToExprClass.toExpr (Regex.Data.Class.perl a) = (Lean.Expr.const `Regex.Data.Class.perl []).app (Lean.toExpr a)

instance Regex.Data.instToExprClass : Lean.ToExpr Class

Equations

• Regex.Data.instToExprClass = { toExpr := Regex.Data.instToExprClass.toExpr, toTypeExpr := Lean.Expr.const `Regex.Data.Class [] }

def Regex.Data.Class.beforeLineBreak : Class

Equations

• Regex.Data.Class.beforeLineBreak = Regex.Data.Class.range (Char.ofNat 0) '\t'

def Regex.Data.Class.afterLineBreak : Class

Equations

• Regex.Data.Class.afterLineBreak = Regex.Data.Class.range '\x0b' (Char.ofNat Char.MAX_UNICODE✝)

def Regex.Data.Class.mem (c : Char) : Class → Bool

Equations

• Regex.Data.Class.mem c (Regex.Data.Class.single a) = (c == a)
• Regex.Data.Class.mem c (Regex.Data.Class.range a a_1) = decide (a ≤ c ∧ c ≤ a_1)
• Regex.Data.Class.mem c (Regex.Data.Class.perl a) = Regex.Data.PerlClass.mem c a

inductive Regex.Data.Classes : Type

• atom : Class → Classes
• complement : Classes → Classes
• union : Classes → Classes → Classes
• intersection : Classes → Classes → Classes
• difference : Classes → Classes → Classes
• symDiff : Classes → Classes → Classes

def Regex.Data.instReprClasses.repr : Classes → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Regex.Data.instReprClasses : Repr Classes

Equations

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

def Regex.Data.instDecidableEqClasses.decEq (x✝ x✝¹ : Classes) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Regex.Data.instDecidableEqClasses.decEq (Regex.Data.Classes.atom a) (Regex.Data.Classes.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (Regex.Data.Classes.atom a) a_1.complement = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (Regex.Data.Classes.atom a) (a_1.union a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (Regex.Data.Classes.atom a) (a_1.intersection a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (Regex.Data.Classes.atom a) (a_1.difference a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (Regex.Data.Classes.atom a) (a_1.symDiff a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq a.complement (Regex.Data.Classes.atom a_1) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq a.complement b.complement = if h : a = b then h ▸ have inst := Regex.Data.instDecidableEqClasses.decEq a a; isTrue ⋯ else isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq a.complement (a_1.union a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq a.complement (a_1.intersection a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq a.complement (a_1.difference a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq a.complement (a_1.symDiff a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.union a_1) (Regex.Data.Classes.atom a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.union a_1) a_2.complement = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.union a_1) (a_2.intersection a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.union a_1) (a_2.difference a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.union a_1) (a_2.symDiff a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.intersection a_1) (Regex.Data.Classes.atom a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.intersection a_1) a_2.complement = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.intersection a_1) (a_2.union a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.intersection a_1) (a_2.difference a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.intersection a_1) (a_2.symDiff a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.difference a_1) (Regex.Data.Classes.atom a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.difference a_1) a_2.complement = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.difference a_1) (a_2.union a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.difference a_1) (a_2.intersection a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.difference a_1) (a_2.symDiff a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.symDiff a_1) (Regex.Data.Classes.atom a_2) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.symDiff a_1) a_2.complement = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.symDiff a_1) (a_2.union a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.symDiff a_1) (a_2.intersection a_3) = isFalse ⋯
• Regex.Data.instDecidableEqClasses.decEq (a.symDiff a_1) (a_2.difference a_3) = isFalse ⋯

instance Regex.Data.instDecidableEqClasses : DecidableEq Classes

Equations

• Regex.Data.instDecidableEqClasses = Regex.Data.instDecidableEqClasses.decEq

def Regex.Data.instInhabitedClasses.default : Classes

Equations

• Regex.Data.instInhabitedClasses.default = Regex.Data.Classes.atom default

instance Regex.Data.instInhabitedClasses : Inhabited Classes

Equations

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

instance Regex.Data.instToExprClasses : Lean.ToExpr Classes

Equations

• Regex.Data.instToExprClasses = { toExpr := Regex.Data.instToExprClasses.toExpr, toTypeExpr := Lean.Expr.const `Regex.Data.Classes [] }

def Regex.Data.instToExprClasses.toExpr : Classes → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Regex.Data.instToExprClasses.toExpr (Regex.Data.Classes.atom a) = (Lean.Expr.const `Regex.Data.Classes.atom []).app (Lean.toExpr a)
• Regex.Data.instToExprClasses.toExpr a.complement = (Lean.Expr.const `Regex.Data.Classes.complement []).app (Regex.Data.instToExprClasses.toExpr a)
• Regex.Data.instToExprClasses.toExpr (a.union a_1) = ((Lean.Expr.const `Regex.Data.Classes.union []).app (Regex.Data.instToExprClasses.toExpr a)).app (Regex.Data.instToExprClasses.toExpr a_1)

def Regex.Data.Classes.mem (c : Char) (e : Classes) : Bool

Equations

• Regex.Data.Classes.mem c (Regex.Data.Classes.atom a) = Regex.Data.Class.mem c a
• Regex.Data.Classes.mem c a.complement = !Regex.Data.Classes.mem c a
• Regex.Data.Classes.mem c (a.union a_1) = (Regex.Data.Classes.mem c a || Regex.Data.Classes.mem c a_1)
• Regex.Data.Classes.mem c (a.intersection a_1) = (Regex.Data.Classes.mem c a && Regex.Data.Classes.mem c a_1)
• Regex.Data.Classes.mem c (a.difference a_1) = (Regex.Data.Classes.mem c a && !Regex.Data.Classes.mem c a_1)
• Regex.Data.Classes.mem c (a.symDiff a_1) = ((Regex.Data.Classes.mem c a || Regex.Data.Classes.mem c a_1) && !(Regex.Data.Classes.mem c a && Regex.Data.Classes.mem c a_1))

instance Regex.Data.instMembershipCharClasses : Membership Char Classes

Equations

• Regex.Data.instMembershipCharClasses = { mem := fun (cs : Regex.Data.Classes) (c : Char) => Regex.Data.Classes.mem c cs = true }

theorem Regex.Data.Classes.mem_mem {c : Char} {cs : Classes} : c ∈ cs ↔ mem c cs = true

@[inline]

instance Regex.Data.instDecidableMemCharClasses {c : Char} {cs : Classes} : Decidable (c ∈ cs)

Equations

• Regex.Data.instDecidableMemCharClasses = match h : Regex.Data.Classes.mem c cs with | true => isTrue h | false => isFalse ⋯