coq 8.7.1 · OCaml Package

val type_of_inductive : Environ.env -> Term.pinductive -> Term.types

val type_of_constructor : Environ.env -> Term.pconstructor -> Term.types

val type_of_constructors : Environ.env -> Term.pinductive -> Term.types array

val arities_of_constructors : 
  Environ.env ->
  Term.pinductive ->
  Term.types array

type inductive_family

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

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

val map_ind_family : 
  (Term.constr -> Term.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 : 
  Term.constr list ->
  int ->
  inductive_family ->
  inductive_family

type inductive_type =

| 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 mis_is_recursive : 
  (Names.inductive
   * Declarations.mutual_inductive_body
   * Declarations.one_inductive_body) ->
  bool

val mis_nf_constructor_type : 
  (Term.pinductive
   * Declarations.mutual_inductive_body
   * Declarations.one_inductive_body) ->
  int ->
  Term.constr

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 : Term.pinductive -> Context.Rel.t

val inductive_paramdecls_env : Environ.env -> Term.pinductive -> Context.Rel.t

val inductive_alldecls : Term.pinductive -> Context.Rel.t

val inductive_alldecls_env : Environ.env -> Term.pinductive -> Context.Rel.t

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 -> Term.sorts_family list

val has_dependent_elim : Declarations.mutual_inductive_body -> bool

val projection_nparams : Names.projection -> int

val projection_nparams_env : Environ.env -> Names.projection -> int

val type_of_projection_knowing_arg : 
  Environ.env ->
  Evd.evar_map ->
  Names.Projection.t ->
  EConstr.t ->
  EConstr.types ->
  Term.types

type constructor_summary = {

cs_cstr : Term.pconstructor;
cs_params : Term.constr list;
cs_nargs : int;
cs_args : Context.Rel.t;
cs_concl_realargs : Term.constr array;

}

val lift_constructor : int -> constructor_summary -> constructor_summary

val get_constructor : 
  (Term.pinductive
   * Declarations.mutual_inductive_body
   * Declarations.one_inductive_body
   * Term.constr list) ->
  int ->
  constructor_summary

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

val get_projections : 
  Environ.env ->
  inductive_family ->
  Names.constant array option

val get_arity : 
  Environ.env ->
  inductive_family ->
  Context.Rel.t * Term.sorts_family

val build_dependent_constructor : constructor_summary -> Term.constr

val build_dependent_inductive : Environ.env -> inductive_family -> Term.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 ->
  Term.sorts ->
  EConstr.types

val build_branch_type : 
  Environ.env ->
  Evd.evar_map ->
  bool ->
  Term.constr ->
  constructor_summary ->
  Term.types

val extract_mrectype : 
  Evd.evar_map ->
  EConstr.t ->
  (Names.inductive * EConstr.EInstance.t) * EConstr.constr list

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) * Term.constr list

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

val arity_of_case_predicate : 
  Environ.env ->
  inductive_family ->
  bool ->
  Term.sorts ->
  Term.types

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

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

val make_case_or_project : 
  Environ.env ->
  Evd.evar_map ->
  inductive_family ->
  Term.case_info ->
  EConstr.constr ->
  EConstr.constr ->
  EConstr.constr array ->
  EConstr.constr

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

val control_only_guard : Environ.env -> Term.types -> unit

val infer_inductive_subtyping_arity_constructor : 
  (Environ.env * Evd.evar_map * Univ.Constraint.t) ->
  (Term.constr -> Term.constr) ->
  Term.types ->
  bool ->
  Context.Rel.t ->
  Environ.env * Evd.evar_map * Univ.Constraint.t

val infer_inductive_subtyping : 
  Environ.env ->
  Evd.evar_map ->
  Entries.mutual_inductive_entry ->
  Entries.mutual_inductive_entry

package coq