Module `Cc_plugin.Ccalgo`Source

Sourcetype pa_constructor = {

cnode : int;
arity : int;
args : int list;

}

Sourcetype cinfo = {

ci_constr : Constr.pconstructor;
ci_arity : int;
ci_nhyps : int;

}

Sourcetype 'a term

Sourcemodule ATerm : sig ... end

Sourcetype ccpattern =

| PApp of ATerm.t * ccpattern list
| PVar of int * ccpattern list

Sourcetype axiom

Sourceval constr_of_axiom : axiom -> Constr.constr

Sourcetype rule =

| Congruence
| Axiom of axiom * bool
| Injection of int * pa_constructor * int * pa_constructor * int

Sourcetype from =

| Goal
| Hyp of Constr.constr
| HeqG of Names.Id.t
| HeqnH of Names.Id.t * Names.Id.t

Sourcetype 'a eq = {

lhs : int;
rhs : int;
rule : 'a;

}

Sourcetype equality = rule eq

Sourcetype disequality = from eq

Sourcetype patt_kind =

| Normal
| Trivial of Constr.types
| Creates_variables

Sourcetype forest

Sourcetype state

Sourcetype explanation =

| Discrimination of int * pa_constructor * int * pa_constructor
| Contradiction of disequality
| Incomplete

Sourceval debug_congruence : CDebug.t

Sourceval forest : state -> forest

Sourceval axioms : forest -> axiom -> ATerm.t * ATerm.t

Sourceval epsilons : forest -> pa_constructor list

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

Source

val add_quant : 
  state ->
  Names.Id.t ->
  bool ->
  (int * patt_kind * ccpattern * patt_kind * ccpattern) ->
  unit

Sourceval tail_pac : pa_constructor -> pa_constructor

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

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/cc_plugin/Cc_plugin/Ccalgo/index.html

Module `Cc_plugin.Ccalgo`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/cc_plugin/Cc_plugin/Ccalgo/index.html

Module Cc_plugin.CcalgoSource

Module `Cc_plugin.Ccalgo`Source