inductive 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).

instance Syntax.instBEqFlavor : BEq Flavor

Equations

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

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

Equations

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

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

Equations

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

instance Syntax.instReprFlavor : Repr Flavor

Equations

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

instance Syntax.instInhabitedFlavor : Inhabited Flavor

Equations

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

instance Syntax.instToStringFlavor : ToString Flavor

Equations

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