Module Frontend.ElabError

module CS := ConcreteSyntax
type t =
  1. | MalformedCase
  2. | InvalidTypeExpression of CS.con
  3. | ExpectedSynthesizableTerm of CS.con_
  4. | CannotEliminate of Basis.Pp.env * S.tp
  5. | ExpectedSimpleInductive of Basis.Pp.env * S.tp
  6. | InvalidModifier of CS.con
  7. | ExpectedFailure of CS.decl
val pp : Stdlib.Format.formatter -> t -> unit
exception ElabError of t * Basis.LexingUtil.span option