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

This release includes a major internal overhaul of the universe/level system, an opt-in binary caching mode for the CLI, and substantial additions to arend-l...

Arend 1.11.0 released

This release focuses primarily on internal enhancements aimed at improving overall stability. Language updates: Introduce Arend server that store the st...

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