inductive Regex.Syntax.Flavor : Type

Flavor of regular expressions

• Pcre : Flavor

  Perl-compatible regular expressions (https://www.pcre.org/current/doc/html/pcre2pattern.html).

• Rust : Flavor

  Rust-compatible regular expressions (https://docs.rs/regex/latest/regex/#syntax).

def Regex.Syntax.instBEqFlavor.beq : Flavor → Flavor → Bool

Equations

• Regex.Syntax.instBEqFlavor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Regex.Syntax.instBEqFlavor : BEq Flavor

Equations

• Regex.Syntax.instBEqFlavor = { beq := Regex.Syntax.instBEqFlavor.beq }

@[instance_reducible]

instance Regex.Syntax.instReprFlavor : Repr Flavor

Equations

• Regex.Syntax.instReprFlavor = { reprPrec := Regex.Syntax.instReprFlavor.repr }

def Regex.Syntax.instReprFlavor.repr : Flavor → Nat → Std.Format

Equations

• Regex.Syntax.instReprFlavor.repr Regex.Syntax.Flavor.Pcre prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.Syntax.Flavor.Pcre")).group prec✝
• Regex.Syntax.instReprFlavor.repr Regex.Syntax.Flavor.Rust prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.Syntax.Flavor.Rust")).group prec✝

@[instance_reducible]

instance Regex.Syntax.instInhabitedFlavor : Inhabited Flavor

Equations

• Regex.Syntax.instInhabitedFlavor = { default := Regex.Syntax.Flavor.Pcre }

@[instance_reducible]

instance Regex.Syntax.instToStringFlavor : ToString Flavor

Equations

• Regex.Syntax.instToStringFlavor = { toString := fun (f : Regex.Syntax.Flavor) => match f with | Regex.Syntax.Flavor.Pcre => "Pcre" | Regex.Syntax.Flavor.Rust => "Rust" }