package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val find_inductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.constr list
val find_coinductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.constr list
val lookup_mind_specif : Environ.env -> Names.inductive -> mind_specif
val instantiate_inductive_constraints : Declarations.mutual_inductive_body -> Univ.Instance.t -> Univ.Constraint.t
type param_univs = (unit -> Univ.Universe.t) list
val make_param_univs : Environ.env -> Constr.constr array -> param_univs
val constrained_type_of_inductive : mind_specif Univ.puniverses -> Constr.types Univ.constrained
val constrained_type_of_inductive_knowing_parameters : mind_specif Univ.puniverses -> param_univs -> Constr.types Univ.constrained
val relevance_of_inductive : Environ.env -> Names.inductive -> Sorts.relevance
val type_of_inductive : mind_specif Univ.puniverses -> Constr.types
val type_of_inductive_knowing_parameters : ?polyprop:bool -> mind_specif Univ.puniverses -> param_univs -> Constr.types
val elim_sort : mind_specif -> Sorts.family
val is_private : mind_specif -> bool
val is_primitive_record : mind_specif -> bool
val constrained_type_of_constructor : Constr.pconstructor -> mind_specif -> Constr.types Univ.constrained
val type_of_constructor : Constr.pconstructor -> mind_specif -> Constr.types
val arities_of_constructors : Constr.pinductive -> mind_specif -> Constr.types array
val type_of_constructors : Constr.pinductive -> mind_specif -> Constr.types array
val arities_of_specif : Names.MutInd.t Univ.puniverses -> mind_specif -> Constr.types array
val inductive_params : mind_specif -> int
val inductive_sort_family : Declarations.one_inductive_body -> Sorts.family
val check_case_info : Environ.env -> Constr.pinductive -> Sorts.relevance -> Constr.case_info -> unit
val is_primitive_positive_container : Environ.env -> Names.Constant.t -> bool
val check_fix : Environ.env -> Constr.fixpoint -> unit
val check_cofix : Environ.env -> Constr.cofixpoint -> unit
exception SingletonInductiveBecomesProp of Names.Id.t
val max_inductive_sort : Sorts.t array -> Univ.Universe.t
type size =
  1. | Large
  2. | Strict
type subterm_spec =
  1. | Subterm of size * Declarations.wf_paths
  2. | Dead_code
  3. | Not_subterm
type guard_env = {
  1. env : Environ.env;
  2. rel_min : int;
  3. genv : subterm_spec Stdlib.Lazy.t list;
}
type stack_element =
  1. | SClosure of guard_env * Constr.constr
  2. | SArg of subterm_spec Stdlib.Lazy.t
val subterm_specif : guard_env -> stack_element list -> Constr.constr -> subterm_spec
val lambda_implicit_lift : int -> Constr.constr -> Constr.constr
val abstract_mind_lc : int -> Int.t -> (Constr.rel_context * Constr.constr) array -> Constr.constr array
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