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...
Recent Posts
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. Language updates: \Prop is now...
Arend 1.0.0 released
The first version of Arend is released! It implements the following features: Path types based on the interval type. Higher inductive types, including ...