package coq-core

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

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
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