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

def Regex.Notation.mkTermOfDecideLt (n m : Nat) : Lean.Term

proof of n < m

example : 1 < 300 := @of_decide_eq_true (1 < 300) (Nat.decLt 1 300) (Eq.refl true)

Equations

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

def Regex.Notation.mkTermOfFin {n : Nat} (f : Fin n) : Lean.Term

Equations

• Regex.Notation.mkTermOfFin f = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `Fin.mk).raw } #[{ raw := (Lean.Syntax.mkNumLit (toString ↑f)).raw }, Regex.Notation.mkTermOfDecideLt (↑f) n]

@[implicit_reducible]

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

Equations

• Regex.Notation.instQuoteFinMkStr1 = { quote := Regex.Notation.mkTermOfFin }

def Regex.Notation.mkTermOfUInt32 (n : UInt32) : Lean.Term

Equations

• Regex.Notation.mkTermOfUInt32 n = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `UInt32.mk).raw } #[Lean.quote `term n.toFin]

@[implicit_reducible]

instance Regex.Notation.instQuoteUInt32MkStr1 : Lean.Quote UInt32

Equations

• Regex.Notation.instQuoteUInt32MkStr1 = { quote := Regex.Notation.mkTermOfUInt32 }

def Regex.Notation.mkTermOfTransition {n : Nat} (t : NFA.Checked.Transition n) : Lean.Term

Equations

• Regex.Notation.mkTermOfTransition t = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.Transition.mk).raw } #[Lean.quote `term t.start, Lean.quote `term t.end, Lean.quote `term t.next]

@[implicit_reducible]

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

Equations

• Regex.Notation.instQuoteTransitionMkStr1 = { quote := Regex.Notation.mkTermOfTransition }

def Regex.Notation.mkTermOfLook (l : NFA.Look) : Lean.Term

Equations

• Regex.Notation.mkTermOfLook NFA.Look.Start = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.Start).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.End = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.End).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.EndWithOptionalLF = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.EndWithOptionalLF).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.StartLF = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.StartLF).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.EndLF = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.EndLF).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.StartCRLF = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.StartCRLF).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.EndCRLF = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.EndCRLF).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.WordUnicode = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.WordUnicode).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.WordUnicodeNegate = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.WordUnicodeNegate).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.WordStartUnicode = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.WordStartUnicode).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.WordEndUnicode = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.WordEndUnicode).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.WordStartHalfUnicode = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.WordStartHalfUnicode).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.WordEndHalfUnicode = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.WordEndHalfUnicode).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.PreviousMatch = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.PreviousMatch).raw } #[]
• Regex.Notation.mkTermOfLook NFA.Look.ClearMatches = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Look.ClearMatches).raw } #[]

@[implicit_reducible]

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

Equations

• Regex.Notation.instQuoteLookMkStr1 = { quote := Regex.Notation.mkTermOfLook }

def Regex.Notation.mkTermOfRole (r : NFA.Capture.Role) : Lean.Term

Equations

• Regex.Notation.mkTermOfRole NFA.Capture.Role.Start = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Capture.Role.Start).raw } #[]
• Regex.Notation.mkTermOfRole NFA.Capture.Role.End = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Capture.Role.End).raw } #[]

@[implicit_reducible]

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

Equations

• Regex.Notation.instQuoteRoleMkStr1 = { quote := Regex.Notation.mkTermOfRole }

def Regex.Notation.mkTermOfCapture (c : NFA.Capture) : Lean.Term

Equations

• Regex.Notation.mkTermOfCapture c = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Capture.mk).raw } #[Regex.Notation.mkTermOfRole c.role, Lean.quote `term c.group]

@[implicit_reducible]

instance Regex.Notation.instQuoteCaptureMkStr1 : Lean.Quote NFA.Capture

Equations

• Regex.Notation.instQuoteCaptureMkStr1 = { quote := Regex.Notation.mkTermOfCapture }

def Regex.Notation.mkTermOfEatMode {n : Nat} (m : NFA.Checked.EatMode n) : Lean.Term

Equations

• Regex.Notation.mkTermOfEatMode (NFA.Checked.EatMode.Until sid) = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.EatMode.Until).raw } #[Regex.Notation.mkTermOfFin sid]
• Regex.Notation.mkTermOfEatMode (NFA.Checked.EatMode.ToLast sid) = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.EatMode.ToLast).raw } #[Regex.Notation.mkTermOfFin sid]

@[implicit_reducible]

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

Equations

• Regex.Notation.instQuoteEatModeMkStr1 = { quote := Regex.Notation.mkTermOfEatMode }

def Regex.Notation.mkTermOfState {n : Nat} (s : NFA.Checked.State n) : Lean.Term

Equations

• One or more equations did not get rendered due to their size.
• Regex.Notation.mkTermOfState (NFA.Checked.State.Empty next) = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.State.Empty).raw } #[Regex.Notation.mkTermOfFin next]
• Regex.Notation.mkTermOfState NFA.Checked.State.Fail = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.State.Fail).raw } #[]
• Regex.Notation.mkTermOfState (NFA.Checked.State.RemoveFrameStep s_2) = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.State.RemoveFrameStep).raw } #[Regex.Notation.mkTermOfFin s_2]
• Regex.Notation.mkTermOfState (NFA.Checked.State.ByteRange t) = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.State.ByteRange).raw } #[Regex.Notation.mkTermOfTransition t]
• Regex.Notation.mkTermOfState (NFA.Checked.State.Union alts) = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.State.Union).raw } #[Lean.quote `term alts]
• Regex.Notation.mkTermOfState (NFA.Checked.State.UnionReverse alts) = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.State.UnionReverse).raw } #[Lean.quote `term alts]
• Regex.Notation.mkTermOfState (NFA.Checked.State.Match id) = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `NFA.Checked.State.Match).raw } #[{ raw := (Regex.Notation.toNumLit id).raw }]

@[implicit_reducible]

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

Equations

• Regex.Notation.instQuoteStateMkStr1 = { quote := Regex.Notation.mkTermOfState }

def Regex.Notation.mkTermIsEq (n : Nat) : Lean.Term

Equations

• Regex.Notation.mkTermIsEq n = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `Eq.refl).raw } #[{ raw := (Regex.Notation.toNumLit n).raw }]

def Regex.Notation.mkTermCapturesValid (captures : Lean.Term) : Lean.Term

Equations

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

def Regex.Notation.mkTermOfNfa (nfa : NFA.Checked.NFA) : Lean.Term

Equations

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

def Regex.Notation.mkTermOfRegex (re : Regex) : Lean.Term

Equations

• Regex.Notation.mkTermOfRegex re = Lean.Syntax.mkApp { raw := (Lean.mkCIdent `Regex.mk).raw } #[Regex.Notation.mkTermOfNfa re.nfa]

@[implicit_reducible]

instance Regex.Notation.instQuoteMkStr1 : Lean.Quote Regex

Equations

• Regex.Notation.instQuoteMkStr1 = { quote := Regex.Notation.mkTermOfRegex }

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

Equations

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

def Lean.Parser.Category.regex : Category

Equations

• Lean.Parser.Category.regex = { }

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))