package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

doc/cc_plugin/Cc_plugin/Ccalgo/index.html

Module Cc_plugin.CcalgoSource

Sourcetype pa_constructor = {
  1. cnode : int;
  2. arity : int;
  3. args : int list;
}
Sourcetype cinfo = {
  1. ci_constr : Constr.pconstructor;
  2. ci_arity : int;
  3. ci_nhyps : int;
}
Sourcetype 'a term
Sourcemodule ATerm : sig ... end
Sourcetype ccpattern =
  1. | PApp of ATerm.t * ccpattern list
  2. | PVar of int * ccpattern list
Sourcetype axiom
Sourceval constr_of_axiom : axiom -> Constr.constr
Sourcetype rule =
  1. | Congruence
  2. | Axiom of axiom * bool
  3. | Injection of int * pa_constructor * int * pa_constructor * int
Sourcetype from =
  1. | Goal
  2. | Hyp of Constr.constr
  3. | HeqG of Names.Id.t
  4. | HeqnH of Names.Id.t * Names.Id.t
Sourcetype 'a eq = {
  1. lhs : int;
  2. rhs : int;
  3. rule : 'a;
}
Sourcetype equality = rule eq
Sourcetype disequality = from eq
Sourcetype patt_kind =
  1. | Normal
  2. | Trivial of Constr.types
  3. | Creates_variables
Sourcetype forest
Sourcetype state
Sourcetype explanation =
  1. | Discrimination of int * pa_constructor * int * pa_constructor
  2. | Contradiction of disequality
  3. | Incomplete of (EConstr.t * int) list
Sourceval debug_congruence : CDebug.t
Sourceval forest : state -> forest
Sourceval axioms : forest -> axiom -> ATerm.t * ATerm.t
Sourceval empty : Environ.env -> Evd.evar_map -> int -> state
Sourceval add_aterm : state -> ATerm.t -> int
Sourceval add_equality : state -> Names.Id.t -> ATerm.t -> ATerm.t -> unit
Sourceval add_disequality : state -> from -> ATerm.t -> ATerm.t -> unit
Sourceval add_quant : state -> Names.Id.t -> bool -> (int * patt_kind * ccpattern * patt_kind * ccpattern) -> unit
Sourceval find_oldest_pac : forest -> int -> pa_constructor -> int
Sourceval aterm : forest -> int -> ATerm.t
Sourceval get_constructor_info : forest -> int -> cinfo
Sourceval subterms : forest -> int -> int * int
Sourceval join_path : forest -> int -> int -> ((int * int) * equality) list * ((int * int) * equality) list
Sourceval execute : bool -> state -> explanation option
Sourceval pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t