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

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

Equations

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

@[implicit_reducible]

instance Regex.Grammar.instBEqExtendedKind : BEq ExtendedKind

Equations

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

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

Equations

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

@[implicit_reducible]

instance Regex.Grammar.instReprExtendedKind : Repr ExtendedKind

Equations

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

structure Regex.Grammar.Parser : Type

State of the parser

• extended : ExtendedKind

  Flag x or 'xx'

@[implicit_reducible]

instance Regex.Grammar.instInhabitedParser : Inhabited Parser

Equations

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

@[reducible, inline]

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

Equations

• Regex.Grammar.ParsecM = ReaderT Regex.Syntax.Flavor (StateT Regex.Grammar.Parser Parser.SimpleCharParser)

def Regex.Grammar.sequence : ParsecM (Lean.TSyntax `sequence)

Equations

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

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.