package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.kernel/Type_errors/index.html

Module Type_errorsSource

Type errors. \label{typeerrors}

Sourcetype 'constr pfix_guard_error =
  1. | NotEnoughAbstractionInFixBody
  2. | RecursionNotOnInductiveType of 'constr
  3. | RecursionOnIllegalTerm of int * Environ.env * 'constr * (int list * int list) Lazy.t
  4. | NotEnoughArgumentsForFixCall of int
  5. | FixpointOnIrrelevantInductive
Sourcetype '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
Sourcetype 'constr pguard_error =
  1. | FixGuardError of 'constr pfix_guard_error
  2. | CoFixGuardError of 'constr pcofix_guard_error
Sourcetype fix_guard_error = Constr.constr pfix_guard_error
Sourcetype cofix_guard_error = Constr.constr pcofix_guard_error
Sourcetype ('constr, 'types) pcant_apply_bad_type = (int * 'constr * 'constr) * ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
Sourcetype ('constr, 'types, 'r) 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 * 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, 'r) Context.pbinder_annot array * int * Environ.env * ('constr, 'types) Environ.punsafe_judgment array
  19. | IllTypedRecBody of int * (Names.Name.t, 'r) Context.pbinder_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. | UndeclaredUniverses of Univ.Level.Set.t
  24. | DisallowedSProp
  25. | BadBinderRelevance of 'r * ('constr, 'types, 'r) Context.Rel.Declaration.pt
  26. | BadCaseRelevance of 'r * '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;
    }
Sourceexception TypeError of Environ.env * type_error
Sourcetype inductive_error =
  1. | NonPos of Constr.constr * Constr.constr
  2. | NotEnoughArgs of Constr.constr * Constr.constr
  3. | NotConstructor of Names.Id.t * Constr.constr * Constr.constr * int * int
  4. | NonPar of 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 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.

Sourceexception InductiveError of Environ.env * inductive_error

Raising functions

Sourceval error_unbound_rel : Environ.env -> int -> 'a
Sourceval error_unbound_var : Environ.env -> Names.variable -> 'a
Sourceval error_not_type : Environ.env -> Environ.unsafe_judgment -> 'a
Sourceval error_assumption : Environ.env -> Environ.unsafe_judgment -> 'a
Sourceval error_reference_variables : Environ.env -> Names.Id.t -> Names.GlobRef.t -> 'a
Sourceval error_elim_arity : Environ.env -> Constr.pinductive -> Constr.constr -> Sorts.t option -> 'a
Sourceval error_case_not_inductive : Environ.env -> Environ.unsafe_judgment -> 'a
Sourceval error_case_on_private_ind : Environ.env -> Names.inductive -> 'a
Sourceval error_number_branches : Environ.env -> Environ.unsafe_judgment -> int -> 'a
Sourceval error_ill_formed_branch : Environ.env -> Constr.constr -> Constr.pconstructor -> Constr.constr -> Constr.constr -> 'a
Sourceval error_generalization : Environ.env -> (Names.Name.t * Constr.types) -> Environ.unsafe_judgment -> 'a
Sourceval error_actual_type : Environ.env -> Environ.unsafe_judgment -> Constr.types -> 'a
Sourceval error_cant_apply_not_functional : Environ.env -> Environ.unsafe_judgment -> Environ.unsafe_judgment array -> 'a
Sourceval error_cant_apply_bad_type : Environ.env -> (int * Constr.constr * Constr.constr) -> Environ.unsafe_judgment -> Environ.unsafe_judgment array -> 'a
Sourceval error_ill_formed_rec_body : Environ.env -> guard_error -> Names.Name.t Constr.binder_annot array -> int -> Environ.env -> Environ.unsafe_judgment array -> 'a
Sourceval error_ill_typed_rec_body : Environ.env -> int -> Names.Name.t Constr.binder_annot array -> Environ.unsafe_judgment array -> Constr.types array -> 'a
Sourceval error_unsatisfied_qconstraints : Environ.env -> Sorts.QConstraints.t -> 'a
Sourceval error_unsatisfied_constraints : Environ.env -> Univ.Constraints.t -> 'a
Sourceval error_undeclared_qualities : Environ.env -> Sorts.QVar.Set.t -> 'a
Sourceval error_undeclared_universes : Environ.env -> Univ.Level.Set.t -> 'a
Sourceval error_disallowed_sprop : Environ.env -> 'a
Sourceval error_bad_binder_relevance : Environ.env -> Sorts.relevance -> Constr.rel_declaration -> 'a
Sourceval error_bad_case_relevance : Environ.env -> Sorts.relevance -> Constr.case -> 'a
Sourceval error_bad_invert : Environ.env -> 'a
Sourceval error_bad_variance : Environ.env -> lev:Univ.Level.t -> expected:UVars.Variance.t -> actual:UVars.Variance.t -> 'a
Sourceval error_undeclared_used_variables : Environ.env -> declared_vars:Names.Id.Set.t -> inferred_vars:Names.Id.Set.t -> 'a
Sourceval map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
Sourceval map_ptype_error : ('r1 -> 'r2) -> ('c -> 'd) -> ('c, 'c, 'r1) ptype_error -> ('d, 'd, 'r2) ptype_error