## Arend 1.10.0 released

Language updates:

Language updates:

- Improved performance
- Inference of unique implicit arguments
- Coercion between paths and functions
- A convenient syntax for defining HITs and pattern matching on them

Plugin updates:

- Proof Search – find declarations by their type (#319)
- Tracer – step-by-step typechecking (#168)
- Re-worked “Arend Messages” panel (#336)
- Printing customization - control over the way of displaying expressions

- Editing:
- Live templates – advanced completion for keywords (#252)
- Optimize imports – detecting and removing unused imports (#11)
- Extract expression to
`\let`

binding - Generate function from a goal with arguments

arend-lib:

- New and improved metas:
- Improved Exists meta and new metas Given and Forall.
- Improved contradiction meta. Now, it can derive contradictions from transitive closure of
`<`

,`<=`

, and`=`

. - New simplify meta.

- Locales:
- The definition of discrete locales and the embedding of rationals into reals.
- The definition of overt locales and open maps.
- The construction of dense-closed and strongly dense-weakly closed factorization systems on the category of locales.
- A proof that nuclei form a frame.
- Limits and colimits of locales.
- A characterization of embeddings of locales: a map of locales is a regular monomorphism if and only if the left adjoint is surjective.
- The definition of (weakly) regular locales and a proof that the locale of reals is regular.
- The definition of Hausdorff locales and a proof that regular locales are Hausdorff.
- The definition of uniform locales and the construction of their completion.

- The definition of abstract reduction systems, second-order term rewriting systems, and a proof that the disjoint union of confluent left-linear systems is confluent.
- The definition of algebraic theories, the category of its models, and a proof that it has all small limits and colimits.
- The preorder of subobjects and regular subobjects.
- The construction of the structure sheaf on the spectrum of a ring.

Nearly every proof assistant has a problem of the discoverability for proven theorems. For instance, try to recall how a lemma describing the commutativity of addition is called in your favorite proof assistant. Is it `add_comm`

? Or `+-comm`

?

The new “Proof Search” action helps in this situation. Invoke it and type in a signature of the declaration you are interested in – the IDE will find the declarations with such a signature:

For more information, please see the full documentation.

The tracer is a new feature that allows you typechecking a declaration step-by-step. At each step, the IDE shows you the typechecking context for the current expression.

To use the tracer:

- Start it via a pop-up menu on a declaration or expression.
- Step through the expressions back and forth, jump to a specific expression via “Run to Cursor”, and stop early if needed.
- Inspect the stack and the context in the editor view at each tracing step.

Compared to the “Show Expression Type” action, the tracer works in more contexts, shows more info, but could be slower.

The “Arend Messages” panel shows current goals and errors. We did a number of changes that are aimed to improve the UX around it:

- Goals and errors are shown in separate panels.
- Goals’ panel is not cleaned up when you remove the goal. It is only removed when a declaration, which contained a goal, has no more errors or other goals.
- Implicit goals (goals without a corresponding
`{?}`

element in the source code) are not shown by default. - The vertical layout is supported.

*This feature is incubating, it may be completely changed in future releases, even minor ones.*

The proof terms which appear during the development of some theory may be quite large. It is often hard to read and understand them, so in order to show these terms to the user we sometimes omit certain subterms. A typical example of a kind of these subterms is implicit arguments – they often may be inferred from the context of the term, so displaying them just adds unnecessary noise. However, we also need a way to show these subterms for the purposes of debugging or better understanding the term semantics. Arend allows to configure pretty-printer options by the eye button in Arend Messages toolwindow.

This approach has a flaw: it is done in an all-or-nothing way. You are offered to display *every* omitted subterm of a certain kind, or not display them at all. Therefore, after changing an option of the pretty printer you become lost in the term.

Arend 1.8.0 offers a solution: we introduce *printing customization* right in the displayed term. You can put a cursor to a source of omittable subterms and then the appeared popup will help you to uncover what was hidden. Currently it works only for implicit arguments and types of parameters in lambda expression.

Live templates are smart code snippets. They speed up editing by providing a completion for common code patterns. This release includes such templates for the majority of Arend keywords:

In addition, you can define your own templates in “Preferences | Editor | Live Templates | Arend”:

Keeping imports clean is easier with this release. The IDE detects unused imports and highlights them in grey color. To remove such imports use the new “Code | Optimize Imports” action:

Aside from just removing, this action can optimize the imports in various ways, for example, import all declarations from a module explicitly. See “Preferences | Editor | Code Style | Arend” for the options.

`\let`

bindingIf you have a complex expression and want to extract some of its parts into `\let`

bindings,
the new “Create \let-binding” intention is there to automate the process:

The “Generate function from a goal” intention is smarter now. When you invoke it on a goal with arguments, the resulting function will get parameters corresponding to those arguments:

Language updates:

Language updates:

Language updates:

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:

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!