package alba

  1. Overview
  2. Docs
type pos = Fmlib.Position.t
type range = pos * pos
type type_in_context = Build_context.type_in_context
type description =
  1. | Overflow
  2. | No_name
  3. | Incomplete_type of type_in_context
  4. | Cannot_infer_bound
  5. | Not_a_function of type_in_context list
  6. | Wrong_type of (type_in_context * type_in_context) list
  7. | Wrong_base of type_in_context list * type_in_context list
  8. | Ambiguous of type_in_context list
  9. | Name_violation of string * string
  10. | Ambiguous_definition
  11. | Wrong_parameter_count of int
  12. | Wrong_parameter_name of string
  13. | Wrong_parameter_type of Alba_core.Term.typ * Alba_core.Gamma.t
  14. | Missing_inductive_type
  15. | No_inductive_type
  16. | Duplicate_inductive
  17. | Duplicate_constructor
  18. | Wrong_type_constructed of Alba_core.Term.typ * Alba_core.Gamma.t
  19. | Negative
  20. | Nested_negative of Alba_core.Inductive.t * int * Alba_core.Gamma.t
  21. | Not_positive of Alba_core.Term.typ * Alba_core.Gamma.t
  22. | Not_yet_implemented of string
type t = range * description
module Print (P : Fmlib.Pretty_printer.SIG) : sig ... end
val string_of_problem : string -> t -> string