package coq

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

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 -> Opaqueproof.opaque Declarations.constant_body -> Opaqueproof.opaque Declarations.constant_body

Is there a actual body in const_body ?

Sourceval constant_has_body : 'a Declarations.constant_body -> bool
Sourceval constant_polymorphic_context : 'a Declarations.constant_body -> Univ.AUContext.t
Sourceval 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.

Sourceval is_opaque : 'a Declarations.constant_body -> bool
Inductive types
Sourceval pp_recarg : Declarations.recarg -> Pp.t
Sourceval pp_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_polymorphic_context : Declarations.mutual_inductive_body -> Univ.AUContext.t
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?

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

Sourceval hcons_const_body : 'a Declarations.constant_body -> 'a Declarations.constant_body
Sourceval 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