Core.RefineError
include module type of RefineErrorData.Data
type t =
| UnboundVariable of Ident.t
| FieldNameMismatches of Ident.user list * Ident.user list
| ExpectedField of Basis.Pp.env
* Core.RefineErrorData.S.tele
* Core.RefineErrorData.S.t
* Ident.t
| ExpectedEqual of Basis.Pp.env
* Core.RefineErrorData.S.tp
* Core.RefineErrorData.S.t
* Core.RefineErrorData.S.t
* Conversion.Error.t
| ExpectedEqualTypes of Basis.Pp.env
* Core.RefineErrorData.S.tp
* Core.RefineErrorData.S.tp
* Conversion.Error.t
| ExpectedConnective of connective * Basis.Pp.env * Core.RefineErrorData.S.tp
| ExpectedDimensionLiteral of int
| ExpectedTrue of Basis.Pp.env * Core.RefineErrorData.S.t
| VirtualType
| HoleNotPermitted of Basis.Pp.env * Core.RefineErrorData.S.tp
| BindingNotFound of Ident.user
| UnexpectedShadowing of Ident.user
| CyclicImport of CodeUnit.CodeUnitID.t
| ErrorsInSection
| UnsolvedHoles of int
| ExpectedSignature of Basis.Pp.env * Core.RefineErrorData.S.tp
| ExpectedKanSignature of Basis.Pp.env * Core.RefineErrorData.S.t
| ExpectedStructure of Basis.Pp.env * Core.RefineErrorData.S.t
val pp : Stdlib.Format.formatter -> t -> unit
exception RefineError of t * Basis.LexingUtil.span option