package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val universes_context : Declarations.universes -> Univ.AUContext.t
val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) Declarations.declaration_arity -> ('c, 'd) Declarations.declaration_arity
val subst_const_body : Mod_subst.substitution -> Opaqueproof.opaque Declarations.constant_body -> Opaqueproof.opaque Declarations.constant_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
val is_opaque : 'a Declarations.constant_body -> bool
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
val inductive_is_cumulative : Declarations.mutual_inductive_body -> bool
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
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