package coq-core

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

The following three functions are similar to the ones defined in Inductive, but they expect an env

Return type as quoted by the user

val type_of_constructors : Environ.env -> Names.inductive EConstr.puniverses -> EConstr.types array
val arities_of_constructors : Environ.env -> Names.inductive EConstr.puniverses -> EConstr.types array

Return constructor types in normal form

type inductive_family

An inductive type with its parameters (transparently supports reasoning either with only recursively uniform parameters or with all parameters including the recursively non-uniform ones

val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
val lift_inductive_family : int -> inductive_family -> inductive_family
val substnl_ind_family : EConstr.constr list -> int -> inductive_family -> inductive_family
val relevance_of_inductive_family : Environ.env -> inductive_family -> EConstr.ERelevance.t
type inductive_type =
  1. | IndType of inductive_family * EConstr.constr list

An inductive type with its parameters and real arguments

val make_ind_type : (inductive_family * EConstr.constr list) -> inductive_type
val dest_ind_type : inductive_type -> inductive_family * EConstr.constr list
val map_inductive_type : (EConstr.constr -> EConstr.constr) -> inductive_type -> inductive_type
val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
val lift_inductive_type : int -> inductive_type -> inductive_type
val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type
val ind_of_ind_type : inductive_type -> Names.inductive
val relevance_of_inductive_type : Environ.env -> inductive_type -> EConstr.ERelevance.t
val mkAppliedInd : inductive_type -> EConstr.constr
val mis_is_recursive_subset : Names.inductive list -> Declarations.wf_paths -> bool
Extract information from an inductive name
val nconstructors : Environ.env -> Names.inductive -> int
  • returns

    number of constructors

val constructors_nrealargs : Environ.env -> Names.inductive -> int array
  • returns

    arity of constructors excluding parameters, excluding local defs

val constructors_nrealdecls : Environ.env -> Names.inductive -> int array
  • returns

    arity of constructors excluding parameters, including local defs

val inductive_nrealargs : Environ.env -> Names.inductive -> int
  • returns

    the arity, excluding params, excluding local defs

val inductive_nrealdecls : Environ.env -> Names.inductive -> int
  • returns

    the arity, excluding params, including local defs

val inductive_nallargs : Environ.env -> Names.inductive -> int
  • returns

    the arity, including params, excluding local defs

val inductive_nalldecls : Environ.env -> Names.inductive -> int
  • returns

    the arity, including params, including local defs

val inductive_nparams : Environ.env -> Names.inductive -> int
  • returns

    nb of params without local defs

val inductive_nparamdecls : Environ.env -> Names.inductive -> int
  • returns

    nb of params with local defs

  • returns

    params context

  • returns

    full arity context, hence with letin

Extract information from a constructor name
val constructor_nallargs : Environ.env -> Names.constructor -> int
  • returns

    param + args without letin

val constructor_nalldecls : Environ.env -> Names.constructor -> int
  • returns

    param + args with letin

val constructor_nrealargs : Environ.env -> Names.constructor -> int
  • returns

    args without letin

val constructor_nrealdecls : Environ.env -> Names.constructor -> int
  • returns

    args with letin

val inductive_alltags : Environ.env -> Names.inductive -> bool list
  • returns

    tags of all decls: true = assumption, false = letin

val constructor_alltags : Environ.env -> Names.constructor -> bool list
val constructor_has_local_defs : Environ.env -> Names.constructor -> bool

Is there local defs in params or args ?

val inductive_has_local_defs : Environ.env -> Names.inductive -> bool
val sorts_below : Sorts.family -> Sorts.family list
val sorts_for_schemes : Declarations.mind_specif -> Sorts.family list
type squash =
  1. | SquashToSet
  2. | SquashToQuality of Sorts.Quality.t
val squash_elim_sort : Environ.env -> Evd.evar_map -> squash -> EConstr.ESorts.t -> Evd.evar_map

Take into account elimination constraints. When there is an elimination constraint and the predicate is underspecified, i.e. a QSort, we make a non-canonical choice for the return type. Incompatible constraints produce a universe inconsistency.

val is_allowed_elimination : Evd.evar_map -> (Declarations.mind_specif * EConstr.EInstance.t) -> EConstr.ESorts.t -> bool
val top_allowed_sort : Environ.env -> Names.inductive -> Sorts.family
val has_dependent_elim : Declarations.mind_specif -> bool

(Co)Inductive records with primitive projections do not have eta-conversion, hence no dependent elimination.

val type_of_projection_knowing_arg : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.t -> EConstr.types -> EConstr.types

Primitive projections

Extract information from an inductive family

type constructor_summary = {
  1. cs_cstr : Names.constructor EConstr.puniverses;
  2. cs_params : EConstr.constr list;
  3. cs_nargs : int;
  4. cs_args : EConstr.rel_context;
  5. cs_concl_realargs : EConstr.constr array;
}
val lift_constructor : int -> constructor_summary -> constructor_summary
val get_constructors : Environ.env -> inductive_family -> constructor_summary array

get_arity returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity

val build_dependent_constructor : constructor_summary -> EConstr.constr
val build_dependent_inductive : Environ.env -> inductive_family -> EConstr.constr
val make_arity_signature : Environ.env -> Evd.evar_map -> bool -> inductive_family -> EConstr.rel_context

Raise Not_found if not given a valid inductive type

instantiate_constructor_params cstr mind params instantiates the type of the given constructor with parameters params

val arity_of_case_predicate : Environ.env -> inductive_family -> bool -> EConstr.ESorts.t -> EConstr.types

Builds the case predicate arity (dependent or not)

Annotation for cases

Make a case or substitute projections if the inductive type is a record with primitive projections. Fail with an error if the elimination is dependent while the inductive type does not allow dependent elimination.

Sometimes make_case_or_project is nicer to call with a pre-built case_invert than inductive_type.

val compute_projections : Environ.env -> Names.inductive -> (EConstr.constr * EConstr.types) array

Given a primitive record type, for every field computes the eta-expanded projection and its type.

val control_only_guard : Environ.env -> Evd.evar_map -> EConstr.types -> unit
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