IntelliJ Arend Features

Code Completion

Code completion is invoked automatically by typing and shows all symbols available in the given context.

Find Usages

To find usages of the symbol at the caret, press Alt+F7. The usages are classified by the context in which they appear.

Quick Documentation

Quick documentation is invoked by Ctrl+Q and shows available information for the symbol at the caret.

Parameter Hints

Parameter hints is invoked by Ctrl+P and shows types of parameters of the definition near the caret.

Class Hierarchy

Class hierarchy is invoked by Ctrl+H and shows subclasses and superclasses of the class at the caret.

Code Formatter

Code formatter helps to format the code while typing. It also can be invoked explicitly by pressing Ctrl+Alt+F7 to format the whole file.

Auto Import

Auto import adds missing imports. To invoke it, press Ctrl+Space on an unresolved symbol. It can also add unambiguous imports on the fly (this can be enabled in Settings | Editor | General | Auto Import).

Pattern Generator

IntelliJ Arend can add missing clauses in pattern matching. It also can split a variable in a pattern into available constructors. The quick fix is invoked by pressing Alt+Enter.

Implement Missing Fields

IntelliJ Arend can add implementation stubs for missing fields. The quick fix is invoked by pressing Alt+Enter.

Move Refactoring

IntelliJ Arend can move a declaration to another module or file. It automatically fixes all references to this declaration. This refactoring can also move a file to another directory.

Background Incremental Typechecking

IntelliJ Arend can typecheck definitions individially. This means that it is enough to rerun the typechecker only on the last modified definition and not the whole file. Also, typechecker is invoked automatically in background.

Show Types

IntelliJ Arend can show types of (sub)expressions. To invoke it press Ctrl+Shift+P on an expression.

Show Expression

IntelliJ Arend can show (normalized) representation of an arbitrary expression. To invoke it press Ctrl+Shift+O on an expression.

Normalize Expression

IntelliJ Arend can replace an expression with its normalized result.

Aliases

Definitions are replaced with their aliases during completion.

Goals

Custom goal solvers can be used to replace goals with expressions.

Redundant Parentheses Inspection

IntelliJ Arend detects and suggests to remove redundant parentheses.

Generate Function

IntelliJ Arend allows to extract goals and selected expressions to a separate function.

Extract to \let-binding

IntelliJ Arend allows to extract selected expressions to a \let-binding.

Unused Imports

IntelliJ Arend detects and suggests to remove import statements that are not used in a module.

Incremental Term Inspection

IntelliJ Arend allows to incrementally reveal hidden information about the term, which reduces visual noise.

Proof Search

IntelliJ Arend provides a flexible search engine that allows to discover theorems by their signature. To invoke it, press Ctrl+Shift+P.

Open Reference

Tracer

Tracer allows to analyze the typechecking process of Arend terms step-by-step.

Change signature

This refactoring can be used to modify the signature of a definition by adding or deleting parameters and changing their explicitness and types. It can be invoked by pressing Ctrl+F6.

Latex documentation

Documentation may contain latex commands which are rendered in the documentation preview.