Idris2-boot/tests
Arnaud Bailly 75b04d867b first stab at syntax highlightin in Emacs
got the basic infrastructure to output syntax highlight in IDE mode
setup but the results are far from being usable, need more work to
understand how to reap information from Metadata
2020-02-29 13:47:27 +01:00
..
chez Some buffer updates 2020-01-31 16:49:31 +00:00
ideMode first stab at syntax highlightin in Emacs 2020-02-29 13:47:27 +01:00
idris2 Update proof tutorial for Idris 2 2020-02-26 12:33:01 +00:00
ttimp More documentation refreshing 2020-02-25 22:18:02 +00:00
typedd-book Better approach to erasure in pattern matching 2020-01-21 18:47:43 +00:00
Main.idr Add default implicit arguments 2020-02-25 14:09:08 +00:00
Makefile Add instructions on how to run a subset of the tests 2019-07-28 20:21:34 +02:00
README.md Add instructions on how to run a subset of the tests 2019-07-28 20:21:34 +02:00

Tests

Note: The commands listed in this section should be run from the repository's root folder.

Run all tests: make test

To run only a subset of the tests use: make test only=NAME. NAME is matched against the path to each test case.

Examples:

  • make test only=chez will run all Chez Scheme tests.
  • make test only=ttimp/basic will run all basic tests for TTImp.
  • make test only=idris2/basic001 will run a specific test.