package coq-core

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

Module InductiveopsSource

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

Return type as quoted by the user

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

Return constructor types in normal form

Sourcetype 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

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

An inductive type with its parameters and real arguments

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

    number of constructors

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

    arity of constructors excluding parameters, excluding local defs

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

    arity of constructors excluding parameters, including local defs

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

    the arity, excluding params, excluding local defs

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

    the arity, excluding params, including local defs

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

    the arity, including params, excluding local defs

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

    the arity, including params, including local defs

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

    nb of params without local defs

Sourceval 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
Sourceval constructor_nallargs : Environ.env -> Names.constructor -> int
  • returns

    param + args without letin

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

    param + args with letin

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

    args without letin

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

    args with letin

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

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

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

Is there local defs in params or args ?

Sourceval inductive_has_local_defs : Environ.env -> Names.inductive -> bool
Sourceval sorts_below : Sorts.family -> Sorts.family list
Sourceval sorts_for_schemes : Declarations.mind_specif -> Sorts.family list
Sourcetype squash =
  1. | SquashToSet
  2. | SquashToQuality of Sorts.Quality.t

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.

Sourceval top_allowed_sort : Environ.env -> Names.inductive -> Sorts.family
Sourceval has_dependent_elim : Declarations.mind_specif -> bool

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

Sourceval 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

Sourcetype 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;
}
Sourceval lift_constructor : int -> constructor_summary -> constructor_summary
Sourceval 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

Sourceval build_dependent_constructor : constructor_summary -> EConstr.constr
Sourceval build_dependent_inductive : Environ.env -> inductive_family -> EConstr.constr
Sourceval 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

Sourceval 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.

Sourceval 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.

Sourceval 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