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 will be the topic of the second part.

2024 1
2022 3
2021 2
2020 5
2019 3

2024

Arend 1.10.0 released

Language updates: Bug fixes and minor improvements Plugin updates: Keyword documentation Improved change signature refactoring Improved move re...

2022

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

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: Type synonyms Arrays Pattern matching in lambdas and \let expressions Multiple level parameters Ability to change levels in sub...

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