Arend 1.7.0 released
- Type synonyms
- Pattern matching in lambdas and \let expressions
- Multiple level parameters
- Ability to change levels in subclasses
- Improved inference of implicit arguments of function types
- New quick-fixes:
- New intentions:
- New “Redundant parentheses” inspection (#237)
- Better support for Prelude (#254)
- Better support for Metas (#261)
- The locale of real numbers
- Compactness of the interval and local compactness of reals
- Spectrum of a ring
- Algebraic rewrite
To bring some declarations to the current scope we use imports. If some imported names are already in scope,
they will be ignored and plugin will show a warning. New “Hide import” quick-fix explicitly hides such names
by adding them to the
Fix failed class instance inference
If you use fields of some class and Arend cannot infer an appropriate instance for it, you will get an error. New quick-fixes help to handle this issue:
- “Import instance” imports an instance available somewhere outside the current scope, say, from arend-lib.
- “Add local instance” adds an implicit parameter of the class type to the current function.
- “Replace local parameter with local instance” is suggested when you already have a parameter that can be used as a classifying field. The fix replaces a type of that parameter with the class type.
Replace with short name
Replaces a reference of the form
B adding an appropriate
This intention comes in 2 flavors. The first one generates a function from a goal:
The second one extracts a selected expression to a separate function:
In both cases you get a function with parameters and return type inferred from the type of the initial expression.
Swap infix operator arguments
Swaps arguments of an infix operator:
Add and Remove clarifying parentheses
Allows adding and removing clarifying parentheses to a sequence of binary operators:
“Redundant parentheses” inspection
Detects redundant parentheses and suggests a fix to remove them:
Better support for Prelude
This release brings a couple of improvements that make Prelude more discoverable:
- Prelude is shown in External Libraries.
- Definitions from Prelude are discoverable via Navigate Symbol, Navigate File, and Find Usages.
Better support for Metas
Discoverability of language extensions (aka metas) is also improved in the following ways:
- Metas are shown as Arend files in External Libraries.
- Metas are discoverable via Navigate Symbol and Navigate File.
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...
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!