def Char.MAX_UNICODE : Nat

Equations

• Char.MAX_UNICODE = 1114111

inductive Regex.Data.PerlClassKind : Type

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

instance Regex.Data.instReprPerlClassKind : Repr PerlClassKind

Equations

• Regex.Data.instReprPerlClassKind = { reprPrec := Regex.Data.reprPerlClassKind✝ }

instance Regex.Data.instDecidableEqPerlClassKind : DecidableEq PerlClassKind

Equations

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

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

structure Regex.Data.PerlClass : Type

• negated : Bool
• kind : PerlClassKind

instance Regex.Data.instReprPerlClass : Repr PerlClass

Equations

• Regex.Data.instReprPerlClass = { reprPrec := Regex.Data.reprPerlClass✝ }

instance Regex.Data.instDecidableEqPerlClass : DecidableEq PerlClass

Equations

• Regex.Data.instDecidableEqPerlClass = Regex.Data.decEqPerlClass✝

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) : s ≤ e → Class
• perl : PerlClass → Class

instance Regex.Data.instDecidableEqClass : DecidableEq Class

Equations

• Regex.Data.instDecidableEqClass = Regex.Data.decEqClass✝

instance Regex.Data.instReprClass : Repr Class

Equations

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

def Regex.Data.Class.beforeLineBreak : Class

Equations

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

def Regex.Data.Class.afterLineBreak : Class

Equations

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

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

Equations

• Regex.Data.Class.mem c (Regex.Data.Class.single c_1) = (c == c_1)
• Regex.Data.Class.mem c (Regex.Data.Class.range s e a) = decide (s ≤ c ∧ c ≤ e)
• Regex.Data.Class.mem c (Regex.Data.Class.perl pc) = Regex.Data.PerlClass.mem c pc

structure Regex.Data.Classes : Type

• negated : Bool
• classes : Array Class

instance Regex.Data.instReprClasses : Repr Classes

Equations

• Regex.Data.instReprClasses = { reprPrec := Regex.Data.reprClasses✝ }

instance Regex.Data.instDecidableEqClasses : DecidableEq Classes

Equations

• Regex.Data.instDecidableEqClasses = Regex.Data.decEqClasses✝

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

Equations

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

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 ⋯