Aleksey Nogin, Vladimir Krupski 
MetaPRL Developer Guide

Currently this guide is just a collection of information that might be useful for MetaPRL developers and advanced users. It is not yet organized in any meaningful way.

This guide contains:

• Indentation and spacing guidelines. Please read them before you start writing any code for MetaPRL.
• Conventions on Using Exceptions in MetaPRL. Again, please read before coding.
• Introduction to MetaPRL Debugging. Please read it before you start debugging your code and especially before you start writing any debugging code yourself.
• Refiners section explains the difference between the "Simple" and "Verbose" refiners.
• MetaPRL Term Modules section explains the difference between the Term_std and Term_ds term modules. It also provides some in-depth information on Term_ds module that you may need if you would want to write some Term_ds-specific code or if you would want to write the code capable of fully utilizing the efficiency advantages of Term_ds:
  • The Definition of Term Types in Term_ds Module
  • Free Variables Calculation in the Term_ds Module
  • Safety Constraints and Invariants of the Term_ds Module
  • The TP-HOLs'2000 paper "Fast Tactic-based Theorem Proving" by A.Nogin and J.Hickey
• Introduction to MetaPRL Profiling. Read it if you want to know where the time gets spent in your code and which branches of your code are taken and how often.