Module Core.RefineError

include module type of RefineErrorData.Data
type connective = [
  1. | `Pi
  2. | `Sg
  3. | `Signature
  4. | `Nat
  5. | `Circle
  6. | `Univ
  7. | `Dim
  8. | `Cof
  9. | `Sub
  10. | `Prf
  11. | `El
  12. | `ElV
  13. | `ElHCom
  14. | `ElExt
]
type t =
  1. | UnboundVariable of Ident.t
  2. | FieldNameMismatches of Ident.user list * Ident.user list
  3. | ExpectedField of Basis.Pp.env * Core.RefineErrorData.S.tele * Core.RefineErrorData.S.t * Ident.t
  4. | ExpectedEqual of Basis.Pp.env * Core.RefineErrorData.S.tp * Core.RefineErrorData.S.t * Core.RefineErrorData.S.t * Conversion.Error.t
  5. | ExpectedEqualTypes of Basis.Pp.env * Core.RefineErrorData.S.tp * Core.RefineErrorData.S.tp * Conversion.Error.t
  6. | ExpectedConnective of connective * Basis.Pp.env * Core.RefineErrorData.S.tp
  7. | ExpectedDimensionLiteral of int
  8. | ExpectedTrue of Basis.Pp.env * Core.RefineErrorData.S.t
  9. | VirtualType
  10. | HoleNotPermitted of Basis.Pp.env * Core.RefineErrorData.S.tp
  11. | BindingNotFound of Ident.user
  12. | UnexpectedShadowing of Ident.user
  13. | CyclicImport of CodeUnit.CodeUnitID.t
  14. | ErrorsInSection
  15. | UnsolvedHoles of int
  16. | ExpectedSignature of Basis.Pp.env * Core.RefineErrorData.S.tp
  17. | ExpectedKanSignature of Basis.Pp.env * Core.RefineErrorData.S.t
  18. | ExpectedStructure of Basis.Pp.env * Core.RefineErrorData.S.t
val pp : Stdlib.Format.formatter -> t -> unit
exception RefineError of t * Basis.LexingUtil.span option