module Theory:sig
..end
Note: this module is highly correlated with the definitions of AAC.v.
This module interfaces with the above Coq module; it provides
facilities to interpret a term with arbitrary operators as an
abstract syntax tree, and to convert an AST into a Coq term
(either using the Coq "raw" terms, as written in the starting
goal, or using the reified Coq datatypes we define in AAC.v).
('a*int) list
), see Matcher.mset
.
mk_mset ty l
constructs a Coq multiset from an OCaml multiset
l
of Coq terms of type ty
val mk_mset : Term.constr -> (Term.constr * int) list -> Term.constr
module Sigma:sig
..end
module Sym:sig
..end
module Stubs:sig
..end
We define a bundle of functions to build reified versions of the
terms (those that will be given to the reflexive decision
procedure). In particular, each field takes as first argument the
index of the symbol rather than the symbol itself.
module Trans:sig
..end