Open ice1000 opened 4 years ago
@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.
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 => {?}
Well, I think I should give an example with the stdlib added
Please complete the following information about the language:
The following are optional, but will help us add the language:
./gradlew jarDep
will give you a jar. This is very lightweight, it won't take you decades to buildjava -jar [cli-full.jar] [your arend file.ard]
:+1: reaction might help.
cli-1.8.0-full.jar
)jar cli-1.8.0-full.jar --test
?)