class Parser.Error (ε : Type u_1) (σ : Type u_2) (τ : outParam (Type u_3)) [Parser.Stream σ τ] : Type (max (max u_1 u_3) u_4)

Parser error class

• unexpected : Stream.Position σ → Option τ → ε

  Unexpected input

• addMessage : ε → Stream.Position σ → String → ε

  Add error message

@[reducible, inline]

abbrev Parser.Error.Trivial : Type

Trivial error type

Equations

• Parser.Error.Trivial = Unit

instance Parser.Error.instTrivial (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Parser.Error Trivial σ τ

Equations

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

@[reducible, inline]

abbrev Parser.Error.Basic (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Type (max u_3 u_2)

Basic error type

Equations

• Parser.Error.Basic σ τ = (Parser.Stream.Position σ × Option τ)

instance Parser.Error.instBasic (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Parser.Error (Basic σ τ) σ τ

Equations

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

instance Parser.Error.instToStringBasicOfReprPosition (σ : Type u_1) (τ : Type u_2) [Repr τ] [Parser.Stream σ τ] [Repr (Stream.Position σ)] : ToString (Basic σ τ)

Equations

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

inductive Parser.Error.Simple (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Type (max u_2 u_3)

Simple error type

• unexpected {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] : Stream.Position σ → Option τ → Simple σ τ

  Unexpected token at position

• addMessage {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] : Simple σ τ → Stream.Position σ → String → Simple σ τ

  Add error message at position

instance Parser.Error.instReprSimpleOfPosition (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] : Repr (Simple σ τ)

Equations

• Parser.Error.instReprSimpleOfPosition σ τ = { reprPrec := Parser.Error.Simple.reprPrec✝ }

instance Parser.Error.instToStringSimpleOfReprPosition (σ : Type u_1) (τ : Type u_2) [Repr τ] [Parser.Stream σ τ] [Repr (Stream.Position σ)] : ToString (Simple σ τ)

Equations

• Parser.Error.instToStringSimpleOfReprPosition σ τ = { toString := Parser.Error.Simple.toString✝ }

instance Parser.Error.instSimple (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Parser.Error (Simple σ τ) σ τ

Equations

• Parser.Error.instSimple σ τ = { unexpected := Parser.Error.Simple.unexpected, addMessage := Parser.Error.Simple.addMessage }