IntelliJ Arend is a plugin for IntelliJ IDEA. To install it, follow the instructions below.
- Download (either community or ultimate version of) IntelliJ IDEA.
- Run Intellij IDEA, choose either Configure | Plugins if you are on a Welcome screen or File | Settings from the main menu if a project is open, go to Plugins tab, search for Arend plugin and install it, restart Intellij IDEA.
- Another way to get the latest version of the plugin is by following instructions on GitHub.
To install the console application, follow the instructions below.
- Download the Arend jar file. You can also get the latest version of the application by following instructions on GitHub.
java -jar Arend.jarto check that everything is alright. You should see an output similar to the following:
$ java -jar Arend.jar [INFO] Loading library prelude [INFO] Loaded library prelude (233ms) Nothing to load
To see command line options, run
java -jar Arend.jar --help.
To create an Arend project, follow instructions here.
The standard library contains a number of essential definitions and proofs, in particular, in constructive algebra and homotopy theory.
It can be downloaded from GitHub (if you are using the IntelliJ plugin, it can be downloaded from the IDE).
This file should be put in some specific directory
libs in which all Arend libraries are stored.
The path to
libs can be specified either with command line option
-L in the console application or in module settings in IntelliJ IDEA.