inductive Syntax.Flavor : Type

Flavor of regular expressions

• Pcre: Syntax.Flavor

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

• Rust: Syntax.Flavor

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

instance Syntax.instBEqFlavor : BEq Syntax.Flavor

Equations

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

instance Syntax.instInhabitedFlavor : Inhabited Syntax.Flavor

Equations

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

instance Syntax.instToStringFlavor : ToString Syntax.Flavor

Equations

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