v1.10

• Keyword documentation
• Improved change signature refactoring
• Improved move refactoring
• Improved parameter hints
• Improved REPL, completion, auto-import, and import optimization
• Improved settings synchronization
• Latex in documentation strings
• Class diagrams
• Quick braces switch intention

v1.9.0

• Inlays for levels, added parameters, and used axioms
• "Change arguments explicitness" refactoring
• "Change signature" refactoring
• Revealing information in error messages

v1.8.0

• Proof Search – find declarations by their type
• Tracer – step-by-step typechecking
• Re-worked “Arend Messages” panel
• Editing:
  • Live templates – advanced completion for keywords
  • Optimize imports – detecting and removing unused imports
  • Extract expression to \let binding
  • Generate function from a goal with arguments

v1.7.0

New quick-fixes:

• Hide import
• Fix failed class instance inference

New intentions:

• Replace with short name
• Generate function
• Swap infix operator arguments
• Add and Remove clarifying parentheses
• New "Redundant parentheses" inspection
• Better support for Prelude
• Better support for Metas

v1.6.0.1

A few bug fixes

v1.6.0

• Quick fixes for "impossible elimination" and "expected constructor" errors

v1.5.0

• Completion of not-imported definitions
• Rainbow highlighting
• arend-lib can be downloaded and upgraded from the IDE

v1.4.1

• Improved implicit arguments inference.
• Fixed a bug aliases in namespace commands.
• Fixed a bug with defined constructors.

v1.4.0

Updates:

• Highlighting and resolving of expressions in error messages.
• Fill goal and refine intentions can be invoked on goals. The latter is implemented through language extensions.
• REPL can be invoked from the main menu.
• Aliases support.
• Improved goto next/previous error.
• Debug for meta definitions.
• Improved documentation support.

v1.3.0

New features and updates:

• Implemented "show type" feature
• Implemented "normalize (sub)expression" feature