package coq

  1. Overview
  2. Docs
package coq
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

Sourceval type_of_inductive : Environ.env -> Constr.pinductive -> Constr.types
Sourceval type_of_constructor : Environ.env -> Constr.pconstructor -> Constr.types

Return type as quoted by the user

Sourceval type_of_constructors : Environ.env -> Constr.pinductive -> Constr.types array
Sourceval arities_of_constructors : Environ.env -> Constr.pinductive -> Constr.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 : Constr.constr list -> int -> inductive_family -> inductive_family
Sourceval relevance_of_inductive_family : Environ.env -> inductive_family -> Sorts.relevance
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 -> Sorts.relevance
Sourceval mkAppliedInd : inductive_type -> EConstr.constr
Sourceval mis_is_recursive_subset : int list -> Declarations.wf_paths -> bool
Extract information from an inductive name
Sourceval nconstructors : Environ.env -> Names.inductive -> int
  • returns

    number of constructors

Sourceval nconstructors_env : Environ.env -> Names.inductive -> int
  • deprecated Alias for Inductiveops.nconstructors
Sourceval constructors_nrealargs : Environ.env -> Names.inductive -> int array
  • returns

    arity of constructors excluding parameters, excluding local defs

Sourceval constructors_nrealargs_env : Environ.env -> Names.inductive -> int array
  • deprecated Alias for Inductiveops.constructors_nrealargs
Sourceval constructors_nrealdecls : Environ.env -> Names.inductive -> int array
  • returns

    arity of constructors excluding parameters, including local defs

Sourceval constructors_nrealdecls_env : Environ.env -> Names.inductive -> int array
  • deprecated Alias for Inductiveops.constructors_nrealdecls
Sourceval inductive_nrealargs : Environ.env -> Names.inductive -> int
  • returns

    the arity, excluding params, excluding local defs

Sourceval inductive_nrealargs_env : Environ.env -> Names.inductive -> int
  • deprecated Alias for Inductiveops.inductive_nrealargs
Sourceval inductive_nrealdecls : Environ.env -> Names.inductive -> int
  • returns

    the arity, excluding params, including local defs

Sourceval inductive_nrealdecls_env : Environ.env -> Names.inductive -> int
  • deprecated Alias for Inductiveops.inductive_nrealdecls
Sourceval inductive_nallargs : Environ.env -> Names.inductive -> int
  • returns

    the arity, including params, excluding local defs

Sourceval inductive_nallargs_env : Environ.env -> Names.inductive -> int
  • deprecated Alias for Inductiveops.inductive_nallargs
Sourceval inductive_nalldecls : Environ.env -> Names.inductive -> int
  • returns

    the arity, including params, including local defs

Sourceval inductive_nalldecls_env : Environ.env -> Names.inductive -> int
  • deprecated Alias for Inductiveops.inductive_nalldecls
Sourceval inductive_nparams : Environ.env -> Names.inductive -> int
  • returns

    nb of params without local defs

Sourceval inductive_nparams_env : Environ.env -> Names.inductive -> int
  • deprecated Alias for Inductiveops.inductive_nparams
Sourceval inductive_nparamdecls : Environ.env -> Names.inductive -> int
  • returns

    nb of params with local defs

Sourceval inductive_nparamdecls_env : Environ.env -> Names.inductive -> int
  • deprecated Alias for Inductiveops.inductive_nparamsdecls
Sourceval inductive_paramdecls : Environ.env -> Constr.pinductive -> Constr.rel_context
  • returns

    params context

Sourceval inductive_paramdecls_env : Environ.env -> Constr.pinductive -> Constr.rel_context
  • deprecated Alias for Inductiveops.inductive_paramsdecl
  • returns

    full arity context, hence with letin

Sourceval inductive_alldecls_env : Environ.env -> Constr.pinductive -> Constr.rel_context
  • deprecated Alias for Inductiveops.inductive_alldecls
Extract information from a constructor name
Sourceval constructor_nallargs : Environ.env -> Names.constructor -> int
  • returns

    param + args without letin

Sourceval constructor_nallargs_env : Environ.env -> Names.constructor -> int
  • deprecated Alias for Inductiveops.constructor_nallargs
Sourceval constructor_nalldecls : Environ.env -> Names.constructor -> int
  • returns

    param + args with letin

Sourceval constructor_nalldecls_env : Environ.env -> Names.constructor -> int
  • deprecated Alias for Inductiveops.constructor_nalldecls
Sourceval constructor_nrealargs : Environ.env -> Names.constructor -> int
  • returns

    args without letin

Sourceval constructor_nrealargs_env : Environ.env -> Names.constructor -> int
  • deprecated Alias for Inductiveops.constructor_nrealargs
Sourceval constructor_nrealdecls : Environ.env -> Names.constructor -> int
  • returns

    args with letin

Sourceval constructor_nrealdecls_env : Environ.env -> Names.constructor -> int
  • deprecated Alias for Inductiveops.constructor_nrealdecls
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 top_allowed_sort : Environ.env -> Names.inductive -> Sorts.family
Sourceval has_dependent_elim : Declarations.mutual_inductive_body -> 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 -> Constr.types

Primitive projections

Extract information from an inductive family

Sourcetype constructor_summary = {
  1. cs_cstr : Constr.pconstructor;
  2. cs_params : Constr.constr list;
  3. cs_nargs : int;
  4. cs_args : Constr.rel_context;
  5. cs_concl_realargs : Constr.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 -> Constr.constr
Sourceval build_dependent_inductive : Environ.env -> inductive_family -> Constr.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

Sourceval arity_of_case_predicate : Environ.env -> inductive_family -> bool -> Sorts.t -> Constr.types

Builds the case predicate arity (dependent or not)

Sourceval type_case_branches_with_names : Environ.env -> Evd.evar_map -> (Constr.pinductive * EConstr.constr list) -> Constr.constr -> Constr.constr -> EConstr.types array * Constr.types

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 -> (Constr.constr * Constr.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