Arend 1.1.0 released

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

Language updates:

Plugin updates:

  • Implemented background typechecking.
  • Implemented pattern generator for missing clauses and case analysis. Note that case analysis currently does not work for \case expressions.
  • Improved class hierarchy.
  • Added gutter icons for subclasses.
  • Improved module configuration dialog.
  • Fixed completion and inline renaming for infix and postfix notation.

2020

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 ↑

2019

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 ↑