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.7.0 released

Language updates: Type synonyms Arrays Pattern matching in lambdas and \let expressions Multiple level parameters Ability to change levels in sub...

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.