Arend 1.7.0 released

Language updates: Type synonyms Arrays Pattern matching in lambdas and \let expressions Multiple level parameters Ability to change levels in subclasses Improved inference of implicit arguments of function types Plugin updates: New quick-fixes: Hide import (#259) Fix failed class instance inference (#114) New intentions: Replace with short name Generate function (#104) Swap infix operator arguments (#44) Add and Remove clarifying parentheses (#238) New “Redundant parentheses” inspection (#237) Better support for Prelude (#254) Better support for Metas (#261) arend-lib: The locale of real numbers Compactness of the interval and local compactness of reals Spectrum of a ring Sheaves Algebraic rewrite Plugin updates Hide import To bring some declarations to the current scope we use imports. If some imported names are already in scope, they will be ignored and plugin will show a warning. New “Hide import” quick-fix explicitly hides such names by adding them to the \hiding directive: Fix failed class instance inference If you use fields of some class and Arend cannot infer an appropriate instance for it, you will get an error. New quick-fixes help to handle this issue: “Import instance” imports an instance available somewhere outside the current scope, say, from arend-lib. “Add local instance” adds an implicit parameter of the class type to the current function. “Replace local parameter with local instance” is suggested when you already have a parameter that can be used as a classifying field. The fix replaces a type of that parameter with the class type. Replace with short name Replaces a reference of the form A.B with B adding an appropriate \open directive: Generate function This intention comes in 2 flavors. The first one generates a function from a goal: The second one extracts a selected expression to a separate function: In both cases you get a function with parameters and return type inferred from the type of the initial expression. Swap infix operator arguments Swaps arguments of an infix operator: Add and Remove clarifying parentheses Allows adding and removing clarifying parentheses to a sequence of binary operators: “Redundant parentheses” inspection Detects redundant parentheses and suggests a fix to remove them: Better support for Prelude This release brings a couple of improvements that make Prelude more discoverable: Prelude is shown in External Libraries. Definitions from Prelude are discoverable via Navigate Symbol, Navigate File, and Find Usages. Better support for Metas Discoverability of language extensions (aka metas) is also improved in the following ways: Metas are shown as Arend files in External Libraries. Metas are discoverable via Navigate Symbol and Navigate File.