Skip to content
master
Switch branches/tags
Go to file
Code

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
api
 
 
 
 
 
 
cli
 
 
lib
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Arend proof assistant

JetBrains offical project Actions Status Gitter

Arend is a theorem prover and a programming language based on Homotopy Type Theory.

Usage

As a binary

You can find release version of Arend binary (a jar file named "Arend.jar") in the release page. The Arend jar can be used to typecheck a library:

$ java -jar Arend.jar [path-to-library]

You can also start a REPL:

$ java -jar Arend.jar -i

If you start the REPL at the root directory of a library, the REPL will load the library. For more information and usage about command line usage of Arend, please refer to --help:

$ java -jar Arend.jar -h

As a library

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

repositories {
    maven { url 'https://jitpack.io' }
}
dependencies {
    // The version of Arend -- can be a short revision, "[branch]-SNAPSHOT",
    // "-SNAPSHOT", or a tag (or a release, like "v1.4.0").
    String arendVersion = "master-SNAPSHOT"
    // Open API for writing Arend extensions
    implementation "com.github.JetBrains.Arend:api:$arendVersion"
    // The generated ANTLR parser
    implementation "com.github.JetBrains.Arend:parser:$arendVersion"
    // The generated protobuf classes
    implementation "com.github.JetBrains.Arend:proto:$arendVersion"
    // The main compiler
    implementation "com.github.JetBrains.Arend:base:$arendVersion"
}

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

repositories {
    maven("https://jitpack.io")
}
dependencies {
    // The version of Arend
    val arendVersion = "master-SNAPSHOT"
    implementation("com.github.JetBrains.Arend:api:$arendVersion")
    implementation("com.github.JetBrains.Arend:parser:$arendVersion")
    implementation("com.github.JetBrains.Arend:proto:$arendVersion")
    implementation("com.github.JetBrains.Arend:base:$arendVersion")
}