package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

doc/funind_plugin/Funind_plugin/Indfun_common/index.html

Module Funind_plugin.Indfun_commonSource

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
Sourceval get_name : Names.Id.t list -> ?default:string -> Names.Name.t -> Names.Name.t
Sourceval array_get_start : 'a array -> 'a array
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
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 = {
  1. function_constant : Names.Constant.t;
  2. graph_ind : Names.inductive;
  3. equation_lemma : Names.Constant.t option;
  4. correctness_lemma : Names.Constant.t option;
  5. completeness_lemma : Names.Constant.t option;
  6. rect_lemma : Names.Constant.t option;
  7. rec_lemma : Names.Constant.t option;
  8. prop_lemma : Names.Constant.t option;
  9. sprop_lemma : Names.Constant.t option;
  10. 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

debugging

Sourceval pr_table : Environ.env -> Evd.evar_map -> Pp.t
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 well_founded_ltof : EConstr.constr Util.delayed
Sourceval evaluable_of_global_reference : Names.GlobRef.t -> Tacred.evaluable_global_reference
Sourceval list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic
Sourcetype tcc_lemma_value =
  1. | Undefined
  2. | Value of Constr.t
  3. | Not_needed
Sourceval funind_purify : ('a -> 'b) -> 'a -> 'b