IntelliJ Arend Features
Code completion is invoked automatically by typing and shows all symbols available in the given context.
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 is invoked by Ctrl+Q and shows available information for the symbol at the caret.
Parameter hints is invoked by Ctrl+P and shows types of parameters of the definition near the caret.
Class hierarchy is invoked by Ctrl+H and shows subclasses and superclasses of the class at the caret.
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 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).
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.
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.
IntelliJ Arend can show types of (sub)expressions. To invoke it press Ctrl+Shift+P on an expression.
IntelliJ Arend can show (normalized) representation of an arbitrary expression. To invoke it press Ctrl+Shift+O on an expression.
Redundant Parentheses Inspection
IntelliJ Arend detects and suggests to remove redundant parentheses.
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.
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.
IntelliJ Arend provides a flexible search engine that allows to discover theorems by their signature. To invoke it, press Ctrl+Shift+P.