Module `Inductiveops`Source

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

val type_of_inductive : 
  Environ.env ->
  Names.inductive EConstr.puniverses ->
  EConstr.types

Source

val e_type_of_inductive : 
  Environ.env ->
  Evd.evar_map ->
  Names.inductive EConstr.puniverses ->
  EConstr.types

Source

val type_of_constructor : 
  Environ.env ->
  Names.constructor EConstr.puniverses ->
  EConstr.types

Return type as quoted by the user

Source

val e_type_of_constructor : 
  Environ.env ->
  Evd.evar_map ->
  Names.constructor EConstr.puniverses ->
  EConstr.types

Source

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

Source

val 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

Source

val make_ind_family : 
  (Names.inductive EConstr.puniverses * EConstr.constr list) ->
  inductive_family

Source

val dest_ind_family : 
  inductive_family ->
  Names.inductive EConstr.puniverses * EConstr.constr list

Source

val map_ind_family : 
  (EConstr.constr -> EConstr.constr) ->
  inductive_family ->
  inductive_family

Sourceval liftn_inductive_family : int -> int -> inductive_family -> inductive_family

Sourceval lift_inductive_family : int -> inductive_family -> inductive_family

Source

val substnl_ind_family : 
  EConstr.constr list ->
  int ->
  inductive_family ->
  inductive_family

Source

val relevance_of_inductive : 
  Environ.env ->
  Names.inductive EConstr.puniverses ->
  EConstr.ERelevance.t

Source

val relevance_of_inductive_family : 
  Environ.env ->
  inductive_family ->
  EConstr.ERelevance.t

Sourcetype inductive_type =

| 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 dest_ind_type : inductive_type -> inductive_family * EConstr.constr list

Source

val map_inductive_type : 
  (EConstr.constr -> EConstr.constr) ->
  inductive_type ->
  inductive_type

Sourceval liftn_inductive_type : int -> int -> inductive_type -> inductive_type

Sourceval lift_inductive_type : int -> inductive_type -> inductive_type

Source

val substnl_ind_type : 
  EConstr.constr list ->
  int ->
  inductive_type ->
  inductive_type

Sourceval ind_of_ind_type : inductive_type -> Names.inductive

Source

val relevance_of_inductive_type : 
  Environ.env ->
  inductive_type ->
  EConstr.ERelevance.t

Sourceval mkAppliedInd : inductive_type -> EConstr.constr

Sourceval dest_recarg : Declarations.recarg Rtree.Kind.t -> Declarations.recarg

Source

val dest_subterms : 
  Declarations.recarg Rtree.Kind.t ->
  Declarations.recarg Rtree.Kind.t array array

Source

val mis_is_recursive_subset : 
  Names.inductive list ->
  Declarations.recarg Rtree.Kind.t ->
  bool

Source

val mis_is_recursive : 
  (Names.inductive
   * Declarations.mutual_inductive_body
   * Declarations.one_inductive_body) ->
  bool

Source

val mis_nf_constructor_type : 
  Names.constructor EConstr.puniverses ->
  (Declarations.mutual_inductive_body * Declarations.one_inductive_body) ->
  EConstr.constr

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

Source

val inductive_paramdecls : 
  Environ.env ->
  Names.inductive EConstr.puniverses ->
  EConstr.rel_context

returns
params context

Source

val inductive_alldecls : 
  Environ.env ->
  Names.inductive EConstr.puniverses ->
  EConstr.rel_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 =

| SquashToSet
| SquashToQuality of Sorts.Quality.t

Sourceval quality_leq : Sorts.Quality.t -> Sorts.Quality.t -> bool

Source

val is_squashed : 
  Evd.evar_map ->
  (Declarations.mind_specif * EConstr.EInstance.t) ->
  squash option

Source

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.

Source

val is_allowed_elimination : 
  Evd.evar_map ->
  (Declarations.mind_specif * EConstr.EInstance.t) ->
  EConstr.ESorts.t ->
  bool

Source

val make_allowed_elimination : 
  Environ.env ->
  Evd.evar_map ->
  (Declarations.mind_specif * EConstr.EInstance.t) ->
  EConstr.ESorts.t ->
  Evd.evar_map option

Returns Some sigma' if the elimination can be allowed, possibly adding constraints in sigma'

Sourceval elim_sort : Declarations.mind_specif -> Sorts.family

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.

Source

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

Sourcetype constructor_summary = {

cs_cstr : Names.constructor EConstr.puniverses;
cs_params : EConstr.constr list;
cs_nargs : int;
cs_args : EConstr.rel_context;
cs_concl_realargs : EConstr.constr array;

}

Sourceval lift_constructor : int -> constructor_summary -> constructor_summary

Source

val get_constructor : 
  (Names.inductive EConstr.puniverses
   * Declarations.mutual_inductive_body
   * Declarations.one_inductive_body
   * EConstr.constr list) ->
  int ->
  constructor_summary

Source

val get_constructors : 
  Environ.env ->
  inductive_family ->
  constructor_summary array

Sourceval get_arity : Environ.env -> inductive_family -> EConstr.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

Sourceval build_dependent_constructor : constructor_summary -> EConstr.constr

Source

val build_dependent_inductive : 
  Environ.env ->
  inductive_family ->
  EConstr.constr

Source

val make_arity_signature : 
  Environ.env ->
  Evd.evar_map ->
  bool ->
  inductive_family ->
  EConstr.rel_context

Source

val make_arity : 
  Environ.env ->
  Evd.evar_map ->
  bool ->
  inductive_family ->
  EConstr.ESorts.t ->
  EConstr.types

Source

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

Source

val find_mrectype : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  (Names.inductive * EConstr.EInstance.t) * EConstr.constr list

Source

val find_mrectype_vect : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  (Names.inductive * EConstr.EInstance.t) * EConstr.constr array

Source

val find_rectype : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  inductive_type

Source

val find_inductive : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  (Names.inductive * EConstr.EInstance.t) * EConstr.constr list

Source

val find_coinductive : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  (Names.inductive * EConstr.EInstance.t) * EConstr.constr list

Source

val instantiate_constructor_params : 
  Names.constructor EConstr.puniverses ->
  Declarations.mind_specif ->
  EConstr.constr list ->
  EConstr.constr

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

Source

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

Builds the case predicate arity (dependent or not)

Source

val make_case_info : 
  Environ.env ->
  Names.inductive ->
  Constr.case_style ->
  Constr.case_info

Annotation for cases

Source

val make_case_or_project : 
  Environ.env ->
  Evd.evar_map ->
  inductive_type ->
  Constr.case_info ->
  (EConstr.constr * EConstr.ERelevance.t) ->
  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.

Source

val simple_make_case_or_project : 
  Environ.env ->
  Evd.evar_map ->
  Constr.case_info ->
  (EConstr.constr * EConstr.ERelevance.t) ->
  EConstr.case_invert ->
  EConstr.constr ->
  EConstr.constr array ->
  EConstr.constr

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

Source

val make_case_invert : 
  Environ.env ->
  Evd.evar_map ->
  inductive_type ->
  case_relevance:EConstr.ERelevance.t ->
  Constr.case_info ->
  EConstr.case_invert

Source

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.

Source

val type_of_inductive_knowing_conclusion : 
  Environ.env ->
  Evd.evar_map ->
  Declarations.mind_specif EConstr.puniverses ->
  EConstr.types ->
  Evd.evar_map * EConstr.types

Sourceval control_only_guard : Environ.env -> Evd.evar_map -> EConstr.types -> unit

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.pretyping/Inductiveops/index.html

Module `Inductiveops`Source

Extract information from an inductive name

Extract information from a constructor name

package rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.pretyping/Inductiveops/index.html

Module InductiveopsSource

Extract information from an inductive name

Extract information from a constructor name

dune-project
Dependency

Module `Inductiveops`Source