IntelliJ Arend Features

Code Completion

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

Show More

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.

Show More

Quick Documentation

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

Show More

Parameter Hints

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

Show More

Class Hierarchy

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

Show More

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.

Show More

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).

Show More

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.

Show More

Implement Missing Fields

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

Show More

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.

Show More

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 More

Show Types

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

Show More

Show Expression

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

Show More

Normalize Expression

IntelliJ Arend can replace an expression with its normalized result.

Show More

Aliases

Definitions are replaced with their aliases during completion.

Show More

Goals

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

Show More

Redundant Parentheses Inspection

IntelliJ Arend detects and suggests to remove redundant parentheses.

Show More

Generate Function

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

Show More

Extract to \let-binding

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

Show More

Unused Imports

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

Show More

Incremental Term Inspection

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

Show More

Tracer

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

Show More