This is a simple major mode for the JonPRL implementation of computational type theory.

Features:

• Completion for keywords, tactics, and operators
• Dynamic generation of yasnippets for each operator
• IMenu
• Simple syntax highlighting, generated from JonPRL’s notion of defined operators
• Eldoc, for showing summaries of tactics or operators in the minibuffer
• Run JonPRL in compilation mode (bound to C-c C-l)
• View JonPRL’s elaborated development (bound to C-c C-c)

To install, arrange for jonprl-mode.el to be on your load-path and then require it.

You may need to customize jonprl-path if the jonprl binary isn’t already on your PATH.

jonprl-mode gets a list of defined operators from JonPRL and uses them to dynamically populate the Yasnippet snippet list. To enable this feature, add yas-minor-mode to your jonprl-mode-hook.

If you use this, then you probably want to set yas-triggers-in-field to t to enable recursive expansion of operators. This gives an experience reminiscent of the Nuprl structure editor.

jonprl-mode reads the list of tactics to highlight from JonPRL itself. If you do something that changes the list of available tactics, restart jonprl-mode with M-x jonprl-mode to re-read them.