Arend proof assistant

Arend is a theorem prover based on Homotopy Type Theory. Visit arend-lang.github.io for more information about the Arend language.

For instructions on building Arend locally, general description of the codebase, there's ARCHITECTURE.md.

Community

• Google
• Telegram
• Gitter

Usage

Arend is under active development, so you may expect to depend your project on a development version of Arend, say, the SNAPSHOT version. This is possible via JitPack, simply add this to your build.gradle:

repositories {
    maven { url 'https://jitpack.io' }
}
dependencies {
    // Open API for writing Arend extensions
    implementation 'com.github.JetBrains.Arend:api:master-SNAPSHOT'
    // The generated ANTLR parser
    implementation 'com.github.JetBrains.Arend:parser:master-SNAPSHOT'
    // The generated protobuf classes
    implementation 'com.github.JetBrains.Arend:proto:master-SNAPSHOT'
    // The main compiler
    implementation 'com.github.JetBrains.Arend:base:master-SNAPSHOT'
}

In case you prefer Gradle Kotlin DSL, use the following syntax in your build.gradle.kts:

repositories {
    maven("https://jitpack.io")
}
dependencies {
    implementation("com.github.JetBrains.Arend:api:master-SNAPSHOT")
    implementation("com.github.JetBrains.Arend:parser:master-SNAPSHOT")
    implementation("com.github.JetBrains.Arend:proto:master-SNAPSHOT")
    implementation("com.github.JetBrains.Arend:base:master-SNAPSHOT")
}