package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
doc/coq-core.kernel/Context/Rel/Declaration/index.html
Module Rel.DeclarationSource
type ('constr, 'types) pt = | LocalAssum of Names.Name.t binder_annot * 'types(*name, type
*)| LocalDef of Names.Name.t binder_annot * 'constr * 'types(*name, value, type
*)
Return the name bound by a given declaration.
Return Some value for local-declarations and None for local-assumptions.
Set the name that is bound by a given declaration.
Set the type of the bound variable in a given declaration.
Return true iff a given declaration is a local assumption.
Return true iff a given declaration is a local definition.
Check whether any term in a given declaration satisfies a given predicate.
Check whether all terms in a given declaration satisfy a given predicate.
Check whether the two given declarations are equal.
Map the name bound by a given declaration.
For local assumptions, this function returns the original local assumptions. For local definitions, this function maps the value in the local definition.
Map the type of the name bound by a given declaration.
Map all terms in a given declaration.
Map all terms, with an heterogeneous function.
Perform a given action on all terms in a given declaration.
Reduce all terms in a given declaration to a single value.