package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

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
Sourceval observe_tac : header:Pp.t -> (Environ.env -> Evd.evar_map -> Pp.t) -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval observe : CDebug.t
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 -> Evaluable.t
Sourceval list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic
Sourceval decompose_lambda_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t EConstr.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