Notation

Notation regex% to build the regular expression at compile time.

def Regex.Notation.toNumLit (n : Nat) : Lean.NumLit

Equations

• Regex.Notation.toNumLit n = Lean.Syntax.mkNumLit n.repr

theorem Regex.Notation.of_decide_eq_true_ext (p : Prop) (inst : Decidable p) : decide p = true → p

instance Regex.Notation.instQuoteFinMkStr1 {n : Nat} : Lean.Quote (Fin n)

Equations

• Regex.Notation.instQuoteFinMkStr1 = Lean.Quote.mk `term Regex.Notation.mkTermOfFin

instance Regex.Notation.instQuoteUInt32MkStr1 : Lean.Quote UInt32

Equations

• Regex.Notation.instQuoteUInt32MkStr1 = Lean.Quote.mk `term Regex.Notation.mkTermOfUInt32

instance Regex.Notation.instQuoteTransitionMkStr1 {n : Nat} : Lean.Quote (NFA.Checked.Transition n)

Equations

• Regex.Notation.instQuoteTransitionMkStr1 = Lean.Quote.mk `term Regex.Notation.mkTermOfTransition

instance Regex.Notation.instQuoteLookMkStr1 : Lean.Quote NFA.Look

Equations

• Regex.Notation.instQuoteLookMkStr1 = Lean.Quote.mk `term Regex.Notation.mkTermOfLook

instance Regex.Notation.instQuoteRoleMkStr1 : Lean.Quote NFA.Capture.Role

Equations

• Regex.Notation.instQuoteRoleMkStr1 = Lean.Quote.mk `term Regex.Notation.mkTermOfRole

instance Regex.Notation.instQuoteEatModeMkStr1 {n : Nat} : Lean.Quote (NFA.Checked.EatMode n)

Equations

• Regex.Notation.instQuoteEatModeMkStr1 = Lean.Quote.mk `term Regex.Notation.mkTermOfEatMode

instance Regex.Notation.instQuoteStateMkStr1 {n : Nat} : Lean.Quote (NFA.Checked.State n)

Equations

• Regex.Notation.instQuoteStateMkStr1 = Lean.Quote.mk `term Regex.Notation.mkTermOfState

instance Regex.Notation.instQuoteMkStr1 : Lean.Quote Regex

Equations

• Regex.Notation.instQuoteMkStr1 = Lean.Quote.mk `term Regex.Notation.mkTermOfRegex

def Lean.Parser.Category.regex : Lean.Parser.Category

Equations

• Lean.Parser.Category.regex = { }

def Regex.Notation.regex.quot : Lean.ParserDescr

Equations

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

def Regex.Notation.regex_ : Lean.ParserDescr

Equations

• Regex.Notation.regex_ = Lean.ParserDescr.node `Regex.Notation.regex_ 1022 (Lean.ParserDescr.const `str)

def Regex.Notation.«termRegex%_» : Lean.ParserDescr

Equations

• Regex.Notation.«termRegex%_» = Lean.ParserDescr.node `Regex.Notation.termRegex%_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "regex%") (Lean.ParserDescr.cat `regex 0))