package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

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

Sources

coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

doc/coq-core.kernel/Declareops/index.html

Module DeclareopsSource

Operations concerning types in Declarations : constant_body, mutual_inductive_body, module_body ...

Arities
Sourceval map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) Declarations.declaration_arity -> ('c, 'd) Declarations.declaration_arity
Constants
Sourceval subst_const_body : Mod_subst.substitution -> Declarations.constant_body -> Declarations.constant_body

Is there a actual body in const_body ?

Sourceval constant_has_body : 'a Declarations.pconstant_body -> bool
Sourceval constant_polymorphic_context : 'a Declarations.pconstant_body -> UVars.AbstractContext.t
Sourceval constant_is_polymorphic : 'a Declarations.pconstant_body -> bool

Is the constant polymorphic?

Return the universe context, in case the definition is polymorphic, otherwise the context is empty.

Sourceval is_opaque : 'a Declarations.pconstant_body -> bool
Inductive types
Sourceval pr_recarg : Declarations.recarg -> Pp.t
Sourceval pr_wf_paths : Declarations.wf_paths -> Pp.t
Sourceval dest_subterms : Declarations.wf_paths -> Declarations.wf_paths list array
Sourceval recarg_length : Declarations.wf_paths -> int -> int
Sourceval subst_mind_body : Mod_subst.substitution -> Declarations.mutual_inductive_body -> Declarations.mutual_inductive_body
Sourceval inductive_is_polymorphic : Declarations.mutual_inductive_body -> bool

Is the inductive polymorphic?

Is the inductive cumulative?

Sourceval inductive_is_cumulative : Declarations.mutual_inductive_body -> bool

Is the inductive cumulative?

Anomaly when not a primitive record or invalid proj_arg

Kernel flags

A default, safe set of flags for kernel type-checking

Hash-consing

Here, strictly speaking, we don't perform true hash-consing of the structure, but simply hash-cons all inner constr and other known elements

Sourceval hcons_const_body : 'a Declarations.pconstant_body -> 'a Declarations.pconstant_body
Sourceval hcons_module_body : Declarations.module_body -> Declarations.module_body