MetaPRL Base Theory

The MetaPRL base theory defines modules that are useful in most logics, including resources that are commonly used to define tactics. There are two parts to the base theory:

1. Basic syntax definitions define the syntax of built-in logical terms and displays.
2. Module resources define procedures that are inherited by all logics, including
   1. The dT tactic
   2. The trivialT and the autoT tactics
   3. Type inference
   4. The proof cache