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

instance Regex.Syntax.Parser.instReprError : Repr Error

Equations

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

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

Equations

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

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

Equations

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

instance Regex.Syntax.Parser.instInhabitedError : Inhabited Error

Equations

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

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.
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.unexpectedEof Regex.Syntax.Parser.Error.unexpectedEof = isTrue ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.unexpectedEof (Regex.Syntax.Parser.Error.unexpectedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.unexpectedEof (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.unexpectedEof (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.unexpectedEof (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.unexpectedEof (Regex.Syntax.Parser.Error.invalidRepetition min max) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.unexpectedEof Regex.Syntax.Parser.Error.expectedEof = isFalse Regex.Syntax.Parser.instDecidableEqError.decEq._proof_6
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedChar c) Regex.Syntax.Parser.Error.unexpectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedChar a) (Regex.Syntax.Parser.Error.unexpectedChar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedChar c) (Regex.Syntax.Parser.Error.unexpectedEscapedChar c_1) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedChar c) (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedChar c) (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedChar c) (Regex.Syntax.Parser.Error.invalidRepetition min max) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedChar c) Regex.Syntax.Parser.Error.expectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) Regex.Syntax.Parser.Error.unexpectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) (Regex.Syntax.Parser.Error.unexpectedChar c_1) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) (Regex.Syntax.Parser.Error.invalidRepetition min max) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) Regex.Syntax.Parser.Error.expectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) Regex.Syntax.Parser.Error.unexpectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) (Regex.Syntax.Parser.Error.unexpectedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) (Regex.Syntax.Parser.Error.invalidRepetition min max) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) Regex.Syntax.Parser.Error.expectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) Regex.Syntax.Parser.Error.unexpectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) (Regex.Syntax.Parser.Error.unexpectedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) (Regex.Syntax.Parser.Error.invalidRepetition min max) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) Regex.Syntax.Parser.Error.expectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRepetition min max) Regex.Syntax.Parser.Error.unexpectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRepetition min max) (Regex.Syntax.Parser.Error.unexpectedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRepetition min max) (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRepetition min max) (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRepetition min max) (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq (Regex.Syntax.Parser.Error.invalidRepetition min max) Regex.Syntax.Parser.Error.expectedEof = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.expectedEof Regex.Syntax.Parser.Error.unexpectedEof = isFalse Regex.Syntax.Parser.instDecidableEqError.decEq._proof_49
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.expectedEof (Regex.Syntax.Parser.Error.unexpectedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.expectedEof (Regex.Syntax.Parser.Error.unexpectedEscapedChar c) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.expectedEof (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.expectedEof (Regex.Syntax.Parser.Error.invalidRange c₁ c₂) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.expectedEof (Regex.Syntax.Parser.Error.invalidRepetition min max) = isFalse ⋯
• Regex.Syntax.Parser.instDecidableEqError.decEq Regex.Syntax.Parser.Error.expectedEof Regex.Syntax.Parser.Error.expectedEof = isTrue ⋯

instance Regex.Syntax.Parser.instDecidableEqError : DecidableEq Error

Equations

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

instance Regex.Syntax.Parser.instToStringError : ToString Error

Equations

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