package coq

  1. Overview
  2. Docs
package coq
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 pa_fun = {
  1. fsym : int;
  2. fnargs : int;
}
Sourcemodule PafMap : CSig.MapS with type key = pa_fun
Sourcetype cinfo = {
  1. ci_constr : Constr.pconstructor;
  2. ci_arity : int;
  3. ci_nhyps : int;
}
Sourcetype 'a term
Sourcemodule ATerm : sig ... end
Sourcemodule Constrhash : Stdlib.Hashtbl.S with type key = Constr.constr
Sourcemodule Termhash : Stdlib.Hashtbl.S with type key = ATerm.t
Sourcetype ccpattern =
  1. | PApp of ATerm.t * ccpattern list
  2. | PVar of int * ccpattern list
Sourcetype rule =
  1. | Congruence
  2. | Axiom of Constr.constr * bool
  3. | Injection of int * pa_constructor * int * pa_constructor * int
Sourcetype from =
  1. | Goal
  2. | Hyp of Constr.constr
  3. | HeqG of Constr.constr
  4. | HeqnH of Constr.constr * Constr.constr
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 quant_eq = {
  1. qe_hyp_id : Names.Id.t;
  2. qe_pol : bool;
  3. qe_nvars : int;
  4. qe_lhs : ccpattern;
  5. qe_lhs_valid : patt_kind;
  6. qe_rhs : ccpattern;
  7. qe_rhs_valid : patt_kind;
}
Sourcetype inductive_status =
  1. | Unknown
  2. | Partial of pa_constructor
  3. | Partial_applied
  4. | Total of int * pa_constructor
Sourcetype representative = {
  1. mutable weight : int;
  2. mutable lfathers : Int.Set.t;
  3. mutable fathers : Int.Set.t;
  4. mutable inductive_status : inductive_status;
  5. class_type : Constr.types;
  6. mutable functions : Int.Set.t PafMap.t;
}
Sourcetype cl =
  1. | Rep of representative
  2. | Eqto of int * equality
Sourcetype vertex =
  1. | Leaf
  2. | Node of int * int
Sourcetype node = {
  1. mutable clas : cl;
  2. mutable cpath : int;
  3. mutable constructors : int PacMap.t;
  4. vertex : vertex;
  5. aterm : ATerm.t;
}
Sourcetype forest = {
  1. mutable max_size : int;
  2. mutable size : int;
  3. mutable map : node array;
  4. axioms : (ATerm.t * ATerm.t) Constrhash.t;
  5. mutable epsilons : pa_constructor list;
  6. syms : int Termhash.t;
}
Sourcetype state
Sourcetype explanation =
  1. | Discrimination of int * pa_constructor * int * pa_constructor
  2. | Contradiction of disequality
  3. | Incomplete
Sourcetype matching_problem
Sourceval debug_congruence : CDebug.t
Sourceval forest : state -> forest
Sourceval axioms : forest -> (ATerm.t * ATerm.t) Constrhash.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 -> Constr.constr -> 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 : forest -> int -> int
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