package coq-core

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

Type errors. \label{typeerrors}

type 'constr pfix_guard_error =
  1. | NotEnoughAbstractionInFixBody
  2. | RecursionNotOnInductiveType of 'constr
  3. | RecursionOnIllegalTerm of int * Environ.env * 'constr * (int list * int list) Stdlib.Lazy.t
  4. | NotEnoughArgumentsForFixCall of int
  5. | FixpointOnIrrelevantInductive
type 'constr pcofix_guard_error =
  1. | CodomainNotInductiveType of 'constr
  2. | NestedRecursiveOccurrences
  3. | UnguardedRecursiveCall of 'constr
  4. | RecCallInTypeOfAbstraction of 'constr
  5. | RecCallInNonRecArgOfConstructor of 'constr
  6. | RecCallInTypeOfDef of 'constr
  7. | RecCallInCaseFun of 'constr
  8. | RecCallInCaseArg of 'constr
  9. | RecCallInCasePred of 'constr
  10. | NotGuardedForm of 'constr
  11. | ReturnPredicateNotCoInductive of 'constr
type 'constr pguard_error =
  1. | FixGuardError of 'constr pfix_guard_error
  2. | CoFixGuardError of 'constr pcofix_guard_error
type fix_guard_error = Constr.constr pfix_guard_error
type cofix_guard_error = Constr.constr pcofix_guard_error
type guard_error = Constr.constr pguard_error
type ('constr, 'types) pcant_apply_bad_type = (int * 'constr * 'constr) * ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
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.t) option
  7. | CaseNotInductive of ('constr, 'types) Environ.punsafe_judgment
  8. | CaseOnPrivateInd of Names.inductive
  9. | WrongCaseInfo of Constr.pinductive * Constr.case_info
  10. | NumberBranches of ('constr, 'types) Environ.punsafe_judgment * int
  11. | IllFormedCaseParams
  12. | IllFormedBranch of 'constr * Constr.pconstructor * 'constr * 'constr
  13. | Generalization of Names.Name.t * 'types * ('constr, 'types) Environ.punsafe_judgment
  14. | ActualType of ('constr, 'types) Environ.punsafe_judgment * 'types
  15. | IncorrectPrimitive of (CPrimitives.op_or_type, 'types) Environ.punsafe_judgment * 'types
  16. | CantApplyBadType of ('constr, 'types) pcant_apply_bad_type
  17. | CantApplyNonFunctional of ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
  18. | IllFormedRecBody of 'constr pguard_error * Names.Name.t Context.binder_annot array * int * Environ.env * ('constr, 'types) Environ.punsafe_judgment array
  19. | IllTypedRecBody of int * Names.Name.t Context.binder_annot array * ('constr, 'types) Environ.punsafe_judgment array * 'types array
  20. | UnsatisfiedQConstraints of Sorts.QConstraints.t
  21. | UnsatisfiedConstraints of Univ.Constraints.t
  22. | UndeclaredQualities of Sorts.QVar.Set.t
  23. | UndeclaredUniverse of Univ.Level.t
  24. | DisallowedSProp
  25. | BadBinderRelevance of Sorts.relevance * ('constr, 'types) Context.Rel.Declaration.pt
  26. | BadCaseRelevance of Sorts.relevance * 'constr
  27. | BadInvert
  28. | BadVariance of {
    1. lev : Univ.Level.t;
    2. expected : UVars.Variance.t;
    3. actual : UVars.Variance.t;
    }
  29. | UndeclaredUsedVariables of {
    1. declared_vars : Names.Id.Set.t;
    2. inferred_vars : Names.Id.Set.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 Sorts.t list * Sorts.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_elim_arity : Environ.env -> Constr.pinductive -> Constr.constr -> (Environ.unsafe_judgment * Sorts.t) option -> 'a
val error_case_not_inductive : Environ.env -> Environ.unsafe_judgment -> 'a
val error_case_on_private_ind : Environ.env -> Names.inductive -> '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_unsatisfied_qconstraints : Environ.env -> Sorts.QConstraints.t -> 'a
val error_unsatisfied_constraints : Environ.env -> Univ.Constraints.t -> 'a
val error_undeclared_qualities : Environ.env -> Sorts.QVar.Set.t -> 'a
val error_undeclared_universe : Environ.env -> Univ.Level.t -> 'a
val error_disallowed_sprop : Environ.env -> 'a
val error_bad_binder_relevance : Environ.env -> Sorts.relevance -> Constr.rel_declaration -> 'a
val error_bad_case_relevance : Environ.env -> Sorts.relevance -> Constr.case -> 'a
val error_bad_invert : Environ.env -> 'a
val error_bad_variance : Environ.env -> lev:Univ.Level.t -> expected:UVars.Variance.t -> actual:UVars.Variance.t -> 'a
val error_undeclared_used_variables : Environ.env -> declared_vars:Names.Id.Set.t -> inferred_vars:Names.Id.Set.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 Blog 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