inductive Regex.Syntax.Parser.Error : Type

• unexpectedEof : Error
• unexpectedChar (c : Char) : Error
• unexpectedEscapedChar (c : Char) : Error
• unexpectedPerlClassInRange (cls : Data.PerlClass) : Error
• invalidRange (c₁ c₂ : Char) : Error
• invalidRepetition (min max : Nat) : Error
• expectedEof : Error
• invalidCodePoint (n : Nat) : Error
• tooManyHexDigits (n : Nat) : Error
• unsupportedCharacterClass : Error

def Regex.Syntax.Parser.instReprError.repr : Error → Nat → Std.Format

Equations

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

instance Regex.Syntax.Parser.instReprError : Repr Error

Equations

• Regex.Syntax.Parser.instReprError = { reprPrec := Regex.Syntax.Parser.instReprError.repr }

instance Regex.Syntax.Parser.instInhabitedError : Inhabited Error

Equations

• Regex.Syntax.Parser.instInhabitedError = { default := Regex.Syntax.Parser.instInhabitedError.default }

def Regex.Syntax.Parser.instInhabitedError.default : Error

Equations

• Regex.Syntax.Parser.instInhabitedError.default = Regex.Syntax.Parser.Error.unexpectedEof

instance Regex.Syntax.Parser.instDecidableEqError : DecidableEq Error

Equations

• Regex.Syntax.Parser.instDecidableEqError = Regex.Syntax.Parser.instDecidableEqError.decEq

def Regex.Syntax.Parser.instDecidableEqError.decEq (x✝ x✝¹ : Error) : Decidable (x✝ = x✝¹)

Equations

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

instance Regex.Syntax.Parser.instToStringError : ToString Error

Equations

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