package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Type errors. \label{typeerrors}

type 'constr pguard_error =
  1. | NotEnoughAbstractionInFixBody
  2. | RecursionNotOnInductiveType of 'constr
  3. | RecursionOnIllegalTerm of int * Environ.env * 'constr * int list * int list
  4. | NotEnoughArgumentsForFixCall of int
    (*

    CoFixpoints

    *)
  5. | CodomainNotInductiveType of 'constr
  6. | NestedRecursiveOccurrences
  7. | UnguardedRecursiveCall of 'constr
  8. | RecCallInTypeOfAbstraction of 'constr
  9. | RecCallInNonRecArgOfConstructor of 'constr
  10. | RecCallInTypeOfDef of 'constr
  11. | RecCallInCaseFun of 'constr
  12. | RecCallInCaseArg of 'constr
  13. | RecCallInCasePred of 'constr
  14. | NotGuardedForm of 'constr
  15. | ReturnPredicateNotCoInductive of 'constr
  16. | FixpointOnIrrelevantInductive
type guard_error = Constr.constr pguard_error
type arity_error =
  1. | NonInformativeToInformative
  2. | StrongEliminationOnNonSmallType
  3. | WrongArity
type ('constr, 'types) ptype_error =
  1. | UnboundRel of int
  2. | UnboundVar of Names.variable
  3. | NotAType of ('constr, 'types) Environ.punsafe_judgment
  4. | BadAssumption of ('constr, 'types) Environ.punsafe_judgment
  5. | ReferenceVariables of Names.Id.t * Names.GlobRef.t
  6. | ElimArity of Constr.pinductive * 'constr * ('constr, 'types) Environ.punsafe_judgment * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
  7. | CaseNotInductive of ('constr, 'types) Environ.punsafe_judgment
  8. | WrongCaseInfo of Constr.pinductive * Constr.case_info
  9. | NumberBranches of ('constr, 'types) Environ.punsafe_judgment * int
  10. | IllFormedBranch of 'constr * Constr.pconstructor * 'constr * 'constr
  11. | Generalization of Names.Name.t * 'types * ('constr, 'types) Environ.punsafe_judgment
  12. | ActualType of ('constr, 'types) Environ.punsafe_judgment * 'types
  13. | IncorrectPrimitive of (CPrimitives.op_or_type, 'types) Environ.punsafe_judgment * 'types
  14. | CantApplyBadType of int * 'constr * 'constr * ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
  15. | CantApplyNonFunctional of ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
  16. | IllFormedRecBody of 'constr pguard_error * Names.Name.t Context.binder_annot array * int * Environ.env * ('constr, 'types) Environ.punsafe_judgment array
  17. | IllTypedRecBody of int * Names.Name.t Context.binder_annot array * ('constr, 'types) Environ.punsafe_judgment array * 'types array
  18. | UnsatisfiedConstraints of Univ.Constraints.t
  19. | UndeclaredUniverse of Univ.Level.t
  20. | DisallowedSProp
  21. | BadRelevance
  22. | BadInvert
  23. | BadVariance of {
    1. lev : Univ.Level.t;
    2. expected : Univ.Variance.t;
    3. actual : Univ.Variance.t;
    }
exception TypeError of Environ.env * type_error
type inductive_error =
  1. | NonPos of Environ.env * Constr.constr * Constr.constr
  2. | NotEnoughArgs of Environ.env * Constr.constr * Constr.constr
  3. | NotConstructor of Environ.env * Names.Id.t * Constr.constr * Constr.constr * int * int
  4. | NonPar of Environ.env * Constr.constr * int * Constr.constr * Constr.constr
  5. | SameNamesTypes of Names.Id.t
  6. | SameNamesConstructors of Names.Id.t
  7. | SameNamesOverlap of Names.Id.t list
  8. | NotAnArity of Environ.env * Constr.constr
  9. | BadEntry
  10. | LargeNonPropInductiveNotInType
  11. | MissingConstraints of Univ.Universe.Set.t * Univ.Universe.t

The different kinds of errors that may result of a malformed inductive definition.

exception InductiveError of inductive_error

Raising functions

val error_unbound_rel : Environ.env -> int -> 'a
val error_unbound_var : Environ.env -> Names.variable -> 'a
val error_not_type : Environ.env -> Environ.unsafe_judgment -> 'a
val error_assumption : Environ.env -> Environ.unsafe_judgment -> 'a
val error_reference_variables : Environ.env -> Names.Id.t -> Names.GlobRef.t -> 'a
val error_case_not_inductive : Environ.env -> Environ.unsafe_judgment -> 'a
val error_number_branches : Environ.env -> Environ.unsafe_judgment -> int -> 'a
val error_ill_formed_branch : Environ.env -> Constr.constr -> Constr.pconstructor -> Constr.constr -> Constr.constr -> 'a
val error_generalization : Environ.env -> (Names.Name.t * Constr.types) -> Environ.unsafe_judgment -> 'a
val error_actual_type : Environ.env -> Environ.unsafe_judgment -> Constr.types -> 'a
val error_cant_apply_not_functional : Environ.env -> Environ.unsafe_judgment -> Environ.unsafe_judgment array -> 'a
val error_cant_apply_bad_type : Environ.env -> (int * Constr.constr * Constr.constr) -> Environ.unsafe_judgment -> Environ.unsafe_judgment array -> 'a
val error_ill_formed_rec_body : Environ.env -> guard_error -> Names.Name.t Context.binder_annot array -> int -> Environ.env -> Environ.unsafe_judgment array -> 'a
val error_ill_typed_rec_body : Environ.env -> int -> Names.Name.t Context.binder_annot array -> Environ.unsafe_judgment array -> Constr.types array -> 'a
val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
val error_unsatisfied_constraints : Environ.env -> Univ.Constraints.t -> 'a
val error_undeclared_universe : Environ.env -> Univ.Level.t -> 'a
val error_disallowed_sprop : Environ.env -> 'a
val error_bad_relevance : Environ.env -> 'a
val error_bad_invert : Environ.env -> 'a
val error_bad_variance : Environ.env -> lev:Univ.Level.t -> expected:Univ.Variance.t -> actual:Univ.Variance.t -> 'a
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct