## MetaPRL Tactic Layer

The proof mechanism used in MetaPRL is LCF-style *tactic*
proving. The *tactic* layer defines functions (called *tacticals*)
to combine tactics, and it also defines term rewriting and *conversionals*.
There are several modules in the tactic layer, including:

**Tacticals****:**
the definition of the basic tactics and tacticals in the base
refinement layer,
**Conversionals****:**
the definition of the basic rewrites in the base refinement layer,
**Sequent:** common operations useful for sequent calculi
**Var:** functions for computing free variables of proof
nodes, and computing "new" variables
**Mptop:** the MetaPRL toploop support