Arend is a theorem prover and a programming language based on Homotopy Type Theory.
- For more information about the Arend language, visit arend-lang.github.io or the documentation.
- For instructions on building Arend locally, general description of the codebase, there's ARCHITECTURE.md.
- For community forums, checkout this link.
- For editing Arend code, we suggest IntelliJ Arend (instructions).
- The standard library of Arend is here. It serves as a math library.
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 -iIf 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 -hArend 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")
}
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent