Unification: standard reformatting, renumbering, step completion, step derivation
Search in the theory
Step Suggestions (Model Based)
Model Generation
Proof Generation
Load/Save additional theorems in .mm compatible format
Prerequisites
To use this extension, you need to have Node.js installed on your machine. If Node.js is not yet installed, follow the official installation guide: Node.js Installation Guide.
Installation
Launch Visual Studio Code.
Go to the Extensions view by clicking on the square icon on the left sidebar or pressing Ctrl+Shift+X.
Search for "Yamma" in the search bar.
Click on the "Install" button next to the "Yamma" extension.
After the installation, click on the "Reload" button to activate the extension.
Usage
Open a .mmp file in Visual Studio Code
If a file set.mm is found in the same folder, the extension will automatically use it as the underlying theory: it will be loaded, parsed, and verified
If no .mm file is automatically found, click on the Gear icon next to the extension's name and select Extension Settings from the dropdown menu. This action opens the settings for Yamma: here you can insert the exact path to the .mm file to be used
Use the command palette (Ctrl+Shift+P or Cmd+Shift+P on macOS) to access the available commands and features provided by the extension
Utilize the Intellisense capabilities to get suggestions while writing your proofs
Once your proof is complete, you can use the "Unify and store in MMT folder" contextual menu command to generate an MMT file, ready to be copied and pasted into your main MM file.
Yamma provides the following keyboard commands (on a Mac we may need to use the command key rather than the CTRL key):
