If you use VS Code, you can also install the Imandra IDE Extension plugin to help with development, providing things like completion and syntax highlighting. We also have a version in development which incorporates automatic proof and refutation information as you type. In order to install the standard extension, first follow the instructions above for installing imandra. Then in VSCode itself VSCode go to the extensions view by following the instructions about the Extension Marketplace and searching for
The extension will open automatically when a file with extension
.ire is opened. The extension will look for the correct version of
ocamlmerlin on the opam switch associated with the folder in which the opened
.ire file resides (defaulting to the current global switch). We recommend that the current global switch is that produced by the recommended installation of imandra, as that contains all the artifacts to facilitate correct imandra type inference and other language server features. Below are example images of the type information the Imandra IDE provides in VSCode.