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 the J operator.
- Implemented pattern matching on idp. This feature can be used instead of the J operator to define functions on path types. This is a standard feature in other proof assistants, but was missing from Arend since it has a different definition of path types.
- New keyword \noclassifying can be used to define classes without classifying fields. Such classes are similar to Agda’s modules and Coq’s sections.
- The type of a field can be overridden with a subtype in a subclass using new keyword \override.
- Variables can be eliminated in \case expressions now.
- Implemented constructor synonyms.
- It is possible now to implement fields using pattern matching.
- We decided to make \Prop proof relevant in general (but it is still proof irrelevant in some cases). The implementation in 1.1.0 was incorrect and it turns out that it is impossible to implement it without loss of the normalization property.
- Now, fields and implementations in a class are typechecked in the order they are specified (before now implementations were typechecked after fields).
- Fixed some problems with pattern generator and implemented case split for \Sigma-types and records.
- It is possible now to adjust the verbosity of pretty printer in error messages.
Language updates: Built-in finite types \default implementations \coerce to function types \coerce for fields and constructors \have declaration ...
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 \...
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. ...
The second part of our tutorial is ready.
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...
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...
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 now has proof irrelevant universe of proposition and the plugin can run the typechecker automatically in background.
The first version of Arend is released!