package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
Sourceval observe_tac : header:Pp.t -> (Environ.env -> Evd.evar_map -> Pp.t) -> unit Proofview.tactic -> unit Proofview.tactic
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
Sourceval decompose_lambda_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
Sourcetype tcc_lemma_value =
  1. | Undefined
  2. | Value of Constr.t
  3. | Not_needed
Sourceval funind_purify : ('a -> 'b) -> 'a -> 'b
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct