package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val type_of_inductive : Environ.env -> Constr.pinductive -> Constr.types
val type_of_constructor : Environ.env -> Constr.pconstructor -> Constr.types
val type_of_constructors : Environ.env -> Constr.pinductive -> Constr.types array
val arities_of_constructors : Environ.env -> Constr.pinductive -> Constr.types array
type 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
type inductive_type =
  1. | IndType of inductive_family * EConstr.constr list
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 mkAppliedInd : inductive_type -> EConstr.constr
val mis_is_recursive_subset : int list -> Declarations.wf_paths -> bool
val nconstructors : Names.inductive -> int
val nconstructors_env : Environ.env -> Names.inductive -> int
val constructors_nrealargs : Names.inductive -> int array
val constructors_nrealargs_env : Environ.env -> Names.inductive -> int array
val constructors_nrealdecls : Names.inductive -> int array
val constructors_nrealdecls_env : Environ.env -> Names.inductive -> int array
val inductive_nrealargs : Names.inductive -> int
val inductive_nrealargs_env : Environ.env -> Names.inductive -> int
val inductive_nrealdecls : Names.inductive -> int
val inductive_nrealdecls_env : Environ.env -> Names.inductive -> int
val inductive_nallargs : Names.inductive -> int
val inductive_nallargs_env : Environ.env -> Names.inductive -> int
val inductive_nalldecls : Names.inductive -> int
val inductive_nalldecls_env : Environ.env -> Names.inductive -> int
val inductive_nparams : Names.inductive -> int
val inductive_nparams_env : Environ.env -> Names.inductive -> int
val inductive_nparamdecls : Names.inductive -> int
val inductive_nparamdecls_env : Environ.env -> Names.inductive -> int
val inductive_paramdecls : Constr.pinductive -> Constr.rel_context
val inductive_paramdecls_env : Environ.env -> Constr.pinductive -> Constr.rel_context
val inductive_alldecls : Constr.pinductive -> Constr.rel_context
val inductive_alldecls_env : Environ.env -> Constr.pinductive -> Constr.rel_context
val constructor_nallargs : Names.constructor -> int
val constructor_nallargs_env : Environ.env -> Names.constructor -> int
val constructor_nalldecls : Names.constructor -> int
val constructor_nalldecls_env : Environ.env -> Names.constructor -> int
val constructor_nrealargs : Names.constructor -> int
val constructor_nrealargs_env : Environ.env -> Names.constructor -> int
val constructor_nrealdecls : Names.constructor -> int
val constructor_nrealdecls_env : Environ.env -> Names.constructor -> int
val constructor_has_local_defs : Names.constructor -> bool
val inductive_has_local_defs : Names.inductive -> bool
val allowed_sorts : Environ.env -> Names.inductive -> Sorts.family list
val has_dependent_elim : Declarations.mutual_inductive_body -> bool
val projection_nparams : Names.Projection.t -> int
  • deprecated Use [Projection.npars]
val projection_nparams_env : Environ.env -> Names.Projection.t -> int
  • deprecated Use [Projection.npars]
val type_of_projection_knowing_arg : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.t -> EConstr.types -> Constr.types
type 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;
}
val lift_constructor : int -> constructor_summary -> constructor_summary
val get_constructors : Environ.env -> inductive_family -> constructor_summary array
val get_projections : Environ.env -> Names.inductive -> Names.Projection.Repr.t array option
  • deprecated Use [Environ.get_projections]
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 -> Sorts.t -> EConstr.types
val build_branch_type : Environ.env -> Evd.evar_map -> bool -> Constr.constr -> constructor_summary -> Constr.types
val arity_of_case_predicate : Environ.env -> inductive_family -> bool -> Sorts.t -> Constr.types
val type_case_branches_with_names : Environ.env -> Evd.evar_map -> (Constr.pinductive * EConstr.constr list) -> Constr.constr -> Constr.constr -> Constr.types array * Constr.types
val compute_projections : Environ.env -> Names.inductive -> (Constr.constr * Constr.types) array
val legacy_match_projection : Environ.env -> Names.inductive -> Constr.constr array
val control_only_guard : Environ.env -> Evd.evar_map -> EConstr.types -> unit