package coq
Formal proof management system
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-8.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926
doc/coq-core.pretyping/Typing/index.html
Module TypingSource
This module provides the typing machine with existential variables and universes.
Source
val type_of :
?refresh:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
Evd.evar_map * EConstr.typesTypecheck a term and return its type + updated evars, optionally refreshing universes
Typecheck a type and return its sort
Typecheck a term has a given type (assuming the type is OK)
Type of a variable.
Returns the instantiated type of a metavariable
Source
val solve_evars :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
Evd.evar_map * EConstr.constrSolve existential variables using typing
Source
val check_allowed_sort :
Environ.env ->
Evd.evar_map ->
Constr.pinductive ->
EConstr.constr ->
EConstr.constr ->
Sorts.relevanceRaise an error message if incorrect elimination for this inductive (first constr is term to match, second is return predicate)
Source
val check_type_fixpoint :
?loc:Loc.t ->
Environ.env ->
Evd.evar_map ->
Names.Name.t Context.binder_annot array ->
EConstr.types array ->
EConstr.unsafe_judgment array ->
Evd.evar_mapRaise an error message if bodies have types not unifiable with the expected ones
Source
val judge_of_apply :
Environ.env ->
Evd.evar_map ->
EConstr.unsafe_judgment ->
EConstr.unsafe_judgment array ->
Evd.evar_map * EConstr.unsafe_judgmentSource
val judge_of_abstraction :
Environ.env ->
Names.Name.t ->
EConstr.unsafe_type_judgment ->
EConstr.unsafe_judgment ->
EConstr.unsafe_judgmentSource
val judge_of_product :
Environ.env ->
Names.Name.t ->
EConstr.unsafe_type_judgment ->
EConstr.unsafe_type_judgment ->
EConstr.unsafe_judgmentSource
val judge_of_projection :
Environ.env ->
Evd.evar_map ->
Names.Projection.t ->
EConstr.unsafe_judgment ->
EConstr.unsafe_judgment