About

Arend

Arend implements a version of homotopy type theory with an interval type, which syntax is similar to cubical type theory. This implies several nice properties of path types and allows for a simple and clean definition of higher inductive types (including recursive ones). To learn more about homotopy features implemented in Arend, see Arend Features.

Arend has a powerful class system, which supports Haskell-style instance inference. Class inheritance can be used to define various hierarchies of (algebraic) structures. For a discussion of the class system, see Arend Features.

IntelliJ Arend

IntelliJ Arend is a plugin for IntelliJ IDEA that turns it into a full-fledged IDE for the Arend language. It has basic features such as syntax highlighting, “goto declaration”, and code folding. Moreover, IntelliJ Arend implements the following advanced features:

• Code completion
• Find usages
• Quick documentation
• Parameter hints
• Class hierarchy
• Code formatter
• Auto import
• “Implement missing fields” quick fix
• Move Refactoring
• Incremental typechecking
• Show types
• Show expression
• Normalize expression
• Aliases
• Goals