package coq

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

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

val universes_context : Declarations.universes -> Univ.AUContext.t
Arities
val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) Declarations.declaration_arity -> ('c, 'd) Declarations.declaration_arity
Constants
val subst_const_body : Mod_subst.substitution -> Opaqueproof.opaque Declarations.constant_body -> Opaqueproof.opaque Declarations.constant_body

Is there a actual body in const_body ?

val constant_has_body : 'a Declarations.constant_body -> bool
val constant_polymorphic_context : 'a Declarations.constant_body -> Univ.AUContext.t
val constant_is_polymorphic : 'a Declarations.constant_body -> bool

Is the constant polymorphic?

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

val is_opaque : 'a Declarations.constant_body -> bool
Inductive types
val eq_recarg : Declarations.recarg -> Declarations.recarg -> bool
val pp_recarg : Declarations.recarg -> Pp.t
val pp_wf_paths : Declarations.wf_paths -> Pp.t
val mk_norec : Declarations.wf_paths
val dest_subterms : Declarations.wf_paths -> Declarations.wf_paths list array
val recarg_length : Declarations.wf_paths -> int -> int
val subst_mind_body : Mod_subst.substitution -> Declarations.mutual_inductive_body -> Declarations.mutual_inductive_body
val inductive_polymorphic_context : Declarations.mutual_inductive_body -> Univ.AUContext.t
val inductive_is_polymorphic : Declarations.mutual_inductive_body -> bool

Is the inductive polymorphic?

Is the inductive cumulative?

val inductive_is_cumulative : Declarations.mutual_inductive_body -> bool

Is the inductive cumulative?

val inductive_make_projection : Names.inductive -> Declarations.mutual_inductive_body -> proj_arg:int -> Names.Projection.Repr.t option
val inductive_make_projections : Names.inductive -> Declarations.mutual_inductive_body -> Names.Projection.Repr.t array option
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

val hcons_const_body : 'a Declarations.constant_body -> 'a Declarations.constant_body
val hcons_module_body : Declarations.module_body -> Declarations.module_body
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet 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