Arend 1.10.0 released
Language updates:
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:
- \Prop is now proof irrelevant. In particular, this means that we do not need Path.inProp anymore.
- Right operator sections.
- New function and \case forms: \sfunc and \scase. It is necessary to use these forms for squashed data types
- Improved error messages.
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.
2024
2022
Arend 1.9.0 released
Language updates:
Arend 1.8.0 released
Language updates:
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...
2021
Arend 1.7.0 released
Language updates:
Arend 1.6.0 released
Language updates: Built-in finite types \default implementations \coerce to function types \coerce for fields and constructors \have declaration ...
2020
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. ...
Tutorial Part II
The second part of our tutorial is ready.
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...
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.
Arend 1.0.0 released
The first version of Arend is released!