Module Inductiveops
val type_of_inductive : Environ.env -> Constr.pinductive -> Constr.types
val e_type_of_inductive : Environ.env -> Evd.evar_map -> Names.inductive EConstr.puniverses -> EConstr.types
val type_of_constructor : Environ.env -> Constr.pconstructor -> Constr.types
Return type as quoted by the user
val e_type_of_constructor : Environ.env -> Evd.evar_map -> Names.constructor EConstr.puniverses -> EConstr.types
val type_of_constructors : Environ.env -> Constr.pinductive -> Constr.types array
val arities_of_constructors : Environ.env -> Constr.pinductive -> Constr.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 make_ind_family : (Names.inductive UVars.puniverses * Constr.constr list) -> inductive_family
val dest_ind_family : inductive_family -> Names.inductive UVars.puniverses * Constr.constr list
val map_ind_family : (Constr.constr -> Constr.constr) -> inductive_family -> inductive_family
val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
val lift_inductive_family : int -> inductive_family -> inductive_family
val substnl_ind_family : Constr.constr list -> int -> inductive_family -> inductive_family
val relevance_of_inductive_family : Environ.env -> inductive_family -> Sorts.relevance
type inductive_type
=
|
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 -> Sorts.relevance
val mkAppliedInd : inductive_type -> EConstr.constr
val mis_is_recursive_subset : int list -> Declarations.wf_paths -> bool
val mis_is_recursive : (Names.inductive * Declarations.mutual_inductive_body * Declarations.one_inductive_body) -> bool
val mis_nf_constructor_type : Constr.pconstructor -> (Declarations.mutual_inductive_body * Declarations.one_inductive_body) -> Constr.constr
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
val inductive_paramdecls : Environ.env -> Constr.pinductive -> Constr.rel_context
- returns
params context
val inductive_alldecls : Environ.env -> Constr.pinductive -> Constr.rel_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
=
|
SquashToSet
|
SquashToQuality of Sorts.Quality.t
val is_squashed : Evd.evar_map -> (Declarations.mind_specif * UVars.Instance.t) -> squash option
val is_allowed_elimination : Evd.evar_map -> (Declarations.mind_specif * UVars.Instance.t) -> EConstr.ESorts.t -> bool
val elim_sort : Declarations.mind_specif -> Sorts.family
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 -> Constr.types
Primitive projections
type constructor_summary
=
{
cs_cstr : Constr.pconstructor;
cs_params : Constr.constr list;
cs_nargs : int;
cs_args : Constr.rel_context;
cs_concl_realargs : Constr.constr array;
}
val lift_constructor : int -> constructor_summary -> constructor_summary
val get_constructor : (Constr.pinductive * Declarations.mutual_inductive_body * Declarations.one_inductive_body * Constr.constr list) -> int -> constructor_summary
val get_constructors : Environ.env -> inductive_family -> constructor_summary array
val get_arity : Environ.env -> inductive_family -> Constr.rel_context
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 -> Constr.constr
val build_dependent_inductive : Environ.env -> inductive_family -> Constr.constr
val make_arity_signature : Environ.env -> Evd.evar_map -> bool -> inductive_family -> EConstr.rel_context
val make_arity : Environ.env -> Evd.evar_map -> bool -> inductive_family -> EConstr.ESorts.t -> EConstr.types
val extract_mrectype : Evd.evar_map -> EConstr.t -> (Names.inductive * EConstr.EInstance.t) * EConstr.constr list
Raise
Not_found
if not given a valid inductive type
val find_mrectype : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.constr list
val find_mrectype_vect : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.constr array
val find_rectype : Environ.env -> Evd.evar_map -> EConstr.types -> inductive_type
val find_inductive : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * Constr.constr list
val find_coinductive : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * Constr.constr list
val instantiate_constructor_params : Constr.pconstructor -> Declarations.mind_specif -> Constr.constr list -> Constr.constr
instantiate_constructor_params cstr mind params
instantiates the type of the given constructor with parametersparams
val arity_of_case_predicate : Environ.env -> inductive_family -> bool -> Sorts.t -> Constr.types
Builds the case predicate arity (dependent or not)
val make_case_info : Environ.env -> Names.inductive -> Constr.case_style -> Constr.case_info
Annotation for cases
val make_case_or_project : Environ.env -> Evd.evar_map -> inductive_type -> Constr.case_info -> (EConstr.constr * Sorts.relevance) -> EConstr.constr -> EConstr.constr array -> EConstr.constr
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.
val simple_make_case_or_project : Environ.env -> Evd.evar_map -> Constr.case_info -> (EConstr.constr * Sorts.relevance) -> EConstr.case_invert -> EConstr.constr -> EConstr.constr array -> EConstr.constr
Sometimes
make_case_or_project
is nicer to call with a pre-builtcase_invert
thaninductive_type
.
val make_case_invert : Environ.env -> inductive_type -> case_relevance:Sorts.relevance -> Constr.case_info -> EConstr.case_invert
val 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.
val type_of_inductive_knowing_conclusion : Environ.env -> Evd.evar_map -> Declarations.mind_specif UVars.puniverses -> EConstr.types -> Evd.evar_map * EConstr.types
val control_only_guard : Environ.env -> Evd.evar_map -> EConstr.types -> unit