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 can also be used to implement various decision procedures for proof automation.

Language updates:

  • Implemented language extensions.
  • Arend now shows conditions in goals which makes it easier to write functions over higher inductive types.

Plugin updates:

  • Implemented “show type” feature.
  • Implemented “show (normalized) expression” feature. This can be used to see inferred implicit arguments or the result of invocation of some function.
  • Implemented “replace (sub)expression” feature. This can be used to replace an expression with its normalized result.

2020

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 ↑

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 ↑