Arend

Arend is a theorem prover based on Homotopy Type Theory. It natively supports higher inductive types and a version of cubical syntax. IntelliJ Arend is a plugin for IntelliJ IDEA that turns it into a full-fledged IDE for the Arend language.

Arend Features IntelliJ Arend Features

Arend 1.6.0 released

Language updates: Built-in finite types \default implementations \coerce to function types \coerce for fields and constructors \have declaration ...

Arend 1.5.0 released

Language updates: String literals, which can be used in meta code Meta resolvers, which can be used to modify the scoping rules for meta definitions \...

Arend 1.4.0 released

Language updates: Implicit lambdas. Tests directory can be used to store files with tests, examples, and other code which is not a part of the library. ...

Tutorial Part II

The second part of our tutorial is ready.

Arend 1.3.0 released

We implemented language extensions. This can be used to implement custom operations on the abstract syntax tree which are not supported by the language. They...