Documentation

Regex.Data.Classes

def Char.MAX_UNICODE :

Equations

Char.MAX_UNICODE = 1114111

Instances For

inductive Regex.Data.PerlClassKind :

Instances For

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 ⋯

instance Regex.Data.instInhabitedPerlClassKind :

Inhabited PerlClassKind

Equations

Regex.Data.instInhabitedPerlClassKind = { default := Regex.Data.PerlClassKind.digit }

instance Regex.Data.instToExprPerlClassKind :

Lean.ToExpr PerlClassKind

Equations

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

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

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 == '_')

Instances For

structure Regex.Data.PerlClass :

negated : Bool
kind : PerlClassKind

Instances For

instance Regex.Data.instReprPerlClass :

Equations

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

instance Regex.Data.instDecidableEqPerlClass :

DecidableEq PerlClass

Equations

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

instance Regex.Data.instInhabitedPerlClass :

Inhabited PerlClass

Equations

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

instance Regex.Data.instToExprPerlClass :

Lean.ToExpr PerlClass

Equations

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

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

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

Instances For

inductive Regex.Data.Class :

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

Instances For

instance Regex.Data.instReprClass :

Equations

Regex.Data.instReprClass = { reprPrec := Regex.Data.reprClass✝ }

instance Regex.Data.instDecidableEqClass :

DecidableEq Class

Equations

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

instance Regex.Data.instInhabitedClass :

Inhabited Class

Equations

Regex.Data.instInhabitedClass = { default := Regex.Data.Class.single default }

instance Regex.Data.instToExprClass :

Lean.ToExpr Class

Equations

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

def Regex.Data.Class.beforeLineBreak :

Equations

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

Instances For

def Regex.Data.Class.afterLineBreak :

Equations

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

Instances For

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

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

Instances For

structure Regex.Data.Classes :

negated : Bool
classes : Array Class

Instances For

instance Regex.Data.instReprClasses :

Equations

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

instance Regex.Data.instDecidableEqClasses :

DecidableEq Classes

Equations

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

instance Regex.Data.instInhabitedClasses :

Inhabited Classes

Equations

Regex.Data.instInhabitedClasses = { default := { negated := default, classes := default } }

instance Regex.Data.instToExprClasses :

Lean.ToExpr Classes

Equations

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

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

Equations

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

Instances For

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 ⋯