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: Regex.Grammar.ExtendedKind
• Extended: Regex.Grammar.ExtendedKind
• ExtendedMore: Regex.Grammar.ExtendedKind

instance Regex.Grammar.instBEqExtendedKind : BEq Regex.Grammar.ExtendedKind

Equations

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

instance Regex.Grammar.instReprExtendedKind : Repr Regex.Grammar.ExtendedKind

Equations

• Regex.Grammar.instReprExtendedKind = { reprPrec := Regex.Grammar.reprExtendedKind✝ }

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 Lean.Parsec)

def Regex.Grammar.parse (s : String) (flavor : Syntax.Flavor) (extended : optParam Regex.Grammar.ExtendedKind Regex.Grammar.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.