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