JetBrains/intellij-arend

---

JetBrains/intellij-arend.json

{
  "createdAt": "2017-07-03T03:53:54Z",
  "defaultBranch": "master",
  "description": "Arend plugin for IntelliJ IDEA",
  "fullName": "JetBrains/intellij-arend",
  "homepage": "",
  "language": "Kotlin",
  "name": "intellij-arend",
  "pushedAt": "2025-02-26T10:44:43Z",
  "stargazersCount": 94,
  "topics": [
    "arend",
    "intellij",
    "intellij-plugin"
  ],
  "updatedAt": "2025-11-19T15:55:08Z",
  "url": "https://github.com/JetBrains/intellij-arend"
}

Arend plugin for IntelliJ IDEA

[![Downloads][d-svg]][jb-url] [![Version][v-svg]][jb-url]

[d-svg] !: https://img.shields.io/jetbrains/plugin/d/11162.svg [v-svg] !: https://img.shields.io/jetbrains/plugin/v/11162.svg [jb-url] !: https://plugins.jetbrains.com/plugin/11162

Plugin that implements Arend support in IntelliJ IDEA and other IntelliJ-based products. Arend is a theorem prover based on Homotopy Type Theory. Visit arend-lang.github.io for more information about the Arend language.

Clone

git clone https://github.com/JetBrains/Arend
git clone https://github.com/JetBrains/intellij-arend.git
cd intellij-arend

Building

We use gradle to build the plugin. It comes with a wrapper script (gradlew or gradlew.bat in the root of the repository) which downloads appropriate version of gradle automatically as long as you have JDK (version >= 11) installed.

Common tasks are

• ./gradlew buildPlugin — fully build plugin and create an archive at build/distributions which can be installed into IntelliJ IDEA via Install plugin from disk action found in File | Settings | Plugins.

• ./gradlew runIde — run a development IDE with the plugin installed.

• ./gradlew test — run all tests.

Developing

You can get the latest IntelliJ IDEA Community Edition here.

To import this project in IntelliJ, use File | New | Project from Existing Sources and select the root directory of the plugin source code.

When hacking on the plugin, you may need the following plugins -

• Grammar-Kit - BNF Grammars and JFlex lexers editor. Readable parser/PSI code generator.
• PsiViewer - A Program Structure Interface (PSI) tree viewer.