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

Language updates: Bug fixes and minor improvements Plugin updates: Keyword documentation Improved change signature refactoring Improved move re...

Arend 1.9.0 released

Language updates: Properties in \Sigma-types Definition parameters are visible in the \where block Global level declarations Infix patterns Axiom...

Arend 1.8.0 released

Language updates: Improved performance Inference of unique implicit arguments Coercion between paths and functions A convenient syntax for defining...

New IntelliJ Arend tutorial

There is a new tutorial on interactive theorem proving with IntelliJ Arend. Check it out to learn about the features of IntelliJ Arend that speed-up theorem...

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