Arend 1.9.0 released

Language updates:

Plugin updates:

  • Inlays for levels, added parameters, and used axioms
  • “Change arguments explicitness” refactoring
  • “Change signature” refactoring
  • Revealing information in error messages


  • The definion of modules, algebras, strict domains, polynomials, and various structures on them
  • A synthetic definition of a derivative and its basic properties
  • The definition of real numbers and the construction of the structure of an ordered field on them (except for multiplication).
  • A tactic for solving systems of linear equations
  • The definition of schemes, affine schemes, and a prove that affine schemes are schemes.
  • A partial prove of the univalence for the precategory of ringed locales.


Back to Top ↑


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

Back to Top ↑


Arend 1.6.0 released

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

Back to Top ↑


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

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

The first part of our tutorial is ready

We finished the first part of our new tutorial. It covers all the basic constructions of Arend. It does not mention anything related to homotopy theory. This...

Back to Top ↑


Arend 1.2.0 released

We implemented a few features related to classes and pattern matching. One of these features is pattern matching on idp : a = a, which can be used instead of...

Arend 1.1.0 released

Arend now has proof irrelevant universe of proposition and the plugin can run the typechecker automatically in background.

Back to Top ↑