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. ...
Arend 1.4.0 released
- Implicit lambdas.
- Tests directory can be used to store files with tests, examples, and other code which is not a part of the library.
- Improved pretty printer: if some definition is not available in the current context, it will be replaced with its full name.
- REPL. To run it, use
- Arend now supports unicode symbols through aliases.
- Equality between disjoint constructors is now considered empty.
- Added support for incomplete lambdas, let expressions, and tuples. Missing expressions are treated as goals.
- Implemented tail call optimization.
- Highlighting and resolving of expressions in error messages.
- Fill goal and refine intentions can be invoked on goals. The latter is implemented through language extensions.
- REPL can be invoked from the main menu: Tools | Show Arend REPL.
- Aliases support.
- Improved goto next/previous error. By default, these actions can be invoked by shortcuts Alt+F2 and Alt+Shift+F2.
- To debug meta definitions, you need to specify a path to Arend jar file in the settings on page Language & Frameworks | Arend. To run the debugger, click on the gutter icon near some Arend definition and choose “Debug ‘Typecheck …’”.
- Improved documentation support.
- Goal solvers can be used to replace goals with expressions.
- Arend UI allows meta definitions to interact with the user.
- Level solvers can be used to automatically prove that a type belongs to a certain homotopy level.
- Number type-checker can be used to elaborate numerical literals to arbitrary expressions.
- User data in definitions can be used to store arbitrary user data.
- User data in ContextData can be used to pass information between meta definitions.
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!