Module `Funind_plugin.Indfun_common`Source

Sourceval mk_rel_id : Names.Id.t -> Names.Id.t

Sourceval mk_correct_id : Names.Id.t -> Names.Id.t

Sourceval mk_complete_id : Names.Id.t -> Names.Id.t

Sourceval mk_equation_id : Names.Id.t -> Names.Id.t

Sourceval fresh_id : Names.Id.t list -> string -> Names.Id.t

Sourceval fresh_name : Names.Id.t list -> string -> Names.Name.t

val get_name : 
  Names.Id.t list ->
  ?default:string ->
  Names.Name.t ->
  Names.Name.t

Sourceval array_get_start : 'a array -> 'a array

Sourceval locate_ind : Libnames.qualid -> Names.inductive

Sourceval locate_constant : Libnames.qualid -> Names.Constant.t

Sourceval locate_with_msg : Pp.t -> (Libnames.qualid -> 'a) -> Libnames.qualid -> 'a

Sourceval filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list

Sourceval list_union_eq : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list

Sourceval list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list

Source

val chop_rlambda_n : 
  int ->
  Glob_term.glob_constr ->
  (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr option) list
  * Glob_term.glob_constr

Source

val chop_rprod_n : 
  int ->
  Glob_term.glob_constr ->
  (Names.Name.t * Glob_term.glob_constr) list * Glob_term.glob_constr

Sourceval eq : EConstr.constr Stdlib.Lazy.t

Sourceval refl_equal : EConstr.constr Stdlib.Lazy.t

Sourceval jmeq : unit -> EConstr.constr

Sourceval jmeq_refl : unit -> EConstr.constr

Sourceval make_eq : unit -> EConstr.constr

Sourceval with_full_print : ('a -> 'b) -> 'a -> 'b

Sourcetype function_info = {

function_constant : Names.Constant.t;
graph_ind : Names.inductive;
equation_lemma : Names.Constant.t option;
correctness_lemma : Names.Constant.t option;
completeness_lemma : Names.Constant.t option;
rect_lemma : Names.Constant.t option;
rec_lemma : Names.Constant.t option;
prop_lemma : Names.Constant.t option;
sprop_lemma : Names.Constant.t option;
is_general : bool;

}

Sourceval find_Function_infos : Names.Constant.t -> function_info option

Sourceval find_Function_of_graph : Names.inductive -> function_info option

Sourceval add_Function : bool -> Names.Constant.t -> unit

Sourceval update_Function : function_info -> unit

Sourceval pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t

debugging

Sourceval pr_table : Environ.env -> Evd.evar_map -> Pp.t

Source

val observe_tac : 
  (Environ.env -> Evd.evar_map -> Pp.t) ->
  Tacmach.tactic ->
  Tacmach.tactic

Sourcemodule New : sig ... end

Sourceval observe : Pp.t -> unit

Sourceval do_observe : unit -> bool

Sourceval do_rewrite_dependent : unit -> bool

Sourceexception Building_graph of exn

Sourceexception Defining_principle of exn

Sourceexception ToShow of exn

Sourceval is_strict_tcc : unit -> bool

Sourceval h_intros : Names.Id.t list -> unit Proofview.tactic

Sourceval h_id : Names.Id.t

Sourceval hrec_id : Names.Id.t

Sourceval acc_inv_id : EConstr.constr Util.delayed

Sourceval ltof_ref : Names.GlobRef.t Util.delayed

Sourceval well_founded_ltof : EConstr.constr Util.delayed

Sourceval acc_rel : EConstr.constr Util.delayed

Sourceval well_founded : EConstr.constr Util.delayed

Source

val evaluable_of_global_reference : 
  Names.GlobRef.t ->
  Tacred.evaluable_global_reference

Source

val list_rewrite : 
  bool ->
  (EConstr.constr * bool) list ->
  unit Proofview.tactic

Source

val decompose_lam_n : 
  Evd.evar_map ->
  int ->
  EConstr.t ->
  (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t

Source

val compose_lam : 
  (Names.Name.t Context.binder_annot * EConstr.t) list ->
  EConstr.t ->
  EConstr.t

Source

val compose_prod : 
  (Names.Name.t Context.binder_annot * EConstr.t) list ->
  EConstr.t ->
  EConstr.t

Sourcetype tcc_lemma_value =

| Undefined
| Value of Constr.t
| Not_needed

Sourceval funind_purify : ('a -> 'b) -> 'a -> 'b

Source

val tac_type_of : 
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  Goal.goal Evd.sigma * EConstr.types

Install

Dune Dependency

Authors

Maintainers

Sources

doc/funind_plugin/Funind_plugin/Indfun_common/index.html

Module `Funind_plugin.Indfun_common`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/funind_plugin/Funind_plugin/Indfun_common/index.html

Module Funind_plugin.Indfun_commonSource

Module `Funind_plugin.Indfun_common`Source