package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type pa_constructor = {
  1. cnode : int;
  2. arity : int;
  3. args : int list;
}
type cinfo = {
  1. ci_constr : Constr.pconstructor;
  2. ci_arity : int;
  3. ci_nhyps : int;
}
type 'a term
module ATerm : sig ... end
type ccpattern =
  1. | PApp of ATerm.t * ccpattern list
  2. | PVar of int * ccpattern list
type axiom
val constr_of_axiom : axiom -> Constr.constr
type rule =
  1. | Congruence
  2. | Axiom of axiom * bool
  3. | Injection of int * pa_constructor * int * pa_constructor * int
type from =
  1. | Goal
  2. | Hyp of Constr.constr
  3. | HeqG of Names.Id.t
  4. | HeqnH of Names.Id.t * Names.Id.t
type 'a eq = {
  1. lhs : int;
  2. rhs : int;
  3. rule : 'a;
}
type equality = rule eq
type disequality = from eq
type patt_kind =
  1. | Normal
  2. | Trivial of Constr.types
  3. | Creates_variables
type forest
type state
type explanation =
  1. | Discrimination of int * pa_constructor * int * pa_constructor
  2. | Contradiction of disequality
  3. | Incomplete of (EConstr.t * int) list
val debug_congruence : CDebug.t
val forest : state -> forest
val axioms : forest -> axiom -> ATerm.t * ATerm.t
val empty : Environ.env -> Evd.evar_map -> int -> state
val add_aterm : state -> ATerm.t -> int
val add_equality : state -> Names.Id.t -> ATerm.t -> ATerm.t -> unit
val add_disequality : state -> from -> ATerm.t -> ATerm.t -> unit
val add_quant : state -> Names.Id.t -> bool -> (int * patt_kind * ccpattern * patt_kind * ccpattern) -> unit
val tail_pac : pa_constructor -> pa_constructor
val find_oldest_pac : forest -> int -> pa_constructor -> int
val aterm : forest -> int -> ATerm.t
val get_constructor_info : forest -> int -> cinfo
val subterms : forest -> int -> int * int
val join_path : forest -> int -> int -> ((int * int) * equality) list * ((int * int) * equality) list
val execute : bool -> state -> explanation option
val 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