Add Arend

[ice1000]

trafficstars

Please complete the following information about the language:

• Name: Arend
• Website: https://arend-lang.github.io/
• Language Version: 1.8.0

The following are optional, but will help us add the language:

• Test Frameworks: Like Agda -- not needed
• How to install: clone the source and ./gradlew jarDep will give you a jar. This is very lightweight, it won't take you decades to build
• How to compile/run: java -jar [cli-full.jar] [your arend file.ard]
• Any comments: It supports HoTT in its very first version, it's evolving, it's by JetBrains, it has an official IntelliJ IDEA plugin

---

:+1: reaction might help.

---

• [x] Build Arend v1.8.0 (cli-1.8.0-full.jar)
• [ ] Figure out testing
  • [x] Commands (jar cli-1.8.0-full.jar --test?)
  • [ ] Postprocessing
• [ ] Create container image
• [ ] SVG logo for icon
• [ ] CodeMirror mode

[kazk]

@ice1000 I'll need some examples like how @DonaldKellett did for Lean. It doesn't have to be a repo, but something similar will be awesome. I'll need examples for passing, failing, and any errors.

[ice1000]

You need this file arend.yaml at the project root:

langVersion: 1.3
sourcesDir: src
testsDir: test
binariesDir: .bin

Your project structure:

- /
  - arend.yaml
  - src
    - Solution.ard
  - test
    - Test.ard

Test.ard:

\import Solution

\lemma check : 1 + 1 = 2 => solution

Solution.ard (passing):

\lemma solution : 1 + 1 = 2 => idp

Solution.ard (failing), different types of failures:

\lemma solution : 1 + 1 = 2 => solution

\lemma solution : 1 + 1 = 3 => idp

-- Anticipated initial setup
\lemma solution : 1 + 1 = 2 => {?}

[ice1000]

Well, I think I should give an example with the stdlib added