Arend 1.6.0 released
- Built-in finite types
- \default implementations
- \coerce to function types
- \coerce for fields and constructors
- \have declaration
- Dot-syntax for dynamic definitions
- Added more computational rules for + and - functions
- Quick fixes for “impossible elimination” and “expected constructor” errors
- Pattern typechecker
- Locales and topological spaces
- Functor category
- Euclidean domains and (extended) Euclidean algorithm
- The quotient ring Z/nZ and the field structure on it for prime n
- Solvers for commutative monoids and rings are implemented in the equation meta
- Extensionality meta
- Structure identity principle meta
- simp_coe meta
- cases meta and improved mcases meta
- unfold and unfold_let metas
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!