Parse a regular expressions into a Lean.Syntax tree according to the Syntax.Flavor.

inductive Regex.Grammar.ExtendedKind : Type

https://www.pcre.org/current/doc/html/pcre2pattern.html#internaloptions

• None : ExtendedKind
• Extended : ExtendedKind
• ExtendedMore : ExtendedKind

instance Regex.Grammar.instBEqExtendedKind : BEq ExtendedKind

Equations

• Regex.Grammar.instBEqExtendedKind = { beq := Regex.Grammar.instBEqExtendedKind.beq }

def Regex.Grammar.instBEqExtendedKind.beq : ExtendedKind → ExtendedKind → Bool

Equations

• Regex.Grammar.instBEqExtendedKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Regex.Grammar.instReprExtendedKind.repr : ExtendedKind → Nat → Std.Format

Equations

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

instance Regex.Grammar.instReprExtendedKind : Repr ExtendedKind

Equations

• Regex.Grammar.instReprExtendedKind = { reprPrec := Regex.Grammar.instReprExtendedKind.repr }

instance Regex.Grammar.instInhabitedParser : Inhabited Regex.Grammar.Parser✝

Equations

• Regex.Grammar.instInhabitedParser = { default := { extended := Regex.Grammar.ExtendedKind.None } }

@[reducible, inline]

abbrev Regex.Grammar.ParsecM (α : Type) : Type

Equations

• Regex.Grammar.ParsecM = ReaderT Syntax.Flavor (StateT Regex.Grammar.Parser✝ Std.Internal.Parsec.String.Parser)

def Regex.Grammar.parse (s : String) (flavor : Syntax.Flavor) (extended : ExtendedKind := ExtendedKind.None) : Except String (Lean.TSyntax `sequence)

Parse a PCRE2 regular expressions into a Lean.Syntax tree.

Equations

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