git.iko.soy/Idris-dev
on master help sign in
Add missing test families in test/README.md

It still needs some clarifiations, specifically: - What is the purpose of `disambig`? - How do the `sugar` and `syntax` differ? Also, added a short comment in `disambig002` to clarify what the test does (thanks @christiansen)

commitff7ea9d65b5c32082cd9aabb14250fded98682e3 authorgpyh <yacine.hmito@gmail.com> dateWed 27 Jul 2016, 14:45 (10 years ago) parent181dddb
2 files changed+4
compare with master
unifiedsplit
test/README.md+2 test/disambig002/disambig002.idr+2
test/README.md+2
@@ -8,6 +8,7 @@ Tests are categorised as follows:
88+ *corecords*: Tests for corecord
99+ *delab*: De-elaboration tests
1010+ *directives*: Tests for directives
11++ *disambig*: Disambiguaton tests
1112+ *docs*: Testing documentation functionality
1213+ *dsl*: Embedded DSLs and features to support DSL development
1314+ *effects*: Effects package
@@ -31,6 +32,7 @@ Tests are categorised as follows:
3132+ *regression*: Regression tests, covering previous bug fixes
3233+ *sourceLocation*: Interaction with files from Idris
3334+ *sugar*: Syntactic sugar, syntax extensions
35++ *syntax*: Syntax extensions
3436+ *tactics*: Testing for tactics
3537+ *totality*: Totality checking
3638+ *tutorial*: Examples from the tutorial
test/disambig002/disambig002.idr+2
@@ -2,6 +2,8 @@ import Data.Vect
22import Data.Fin
33import Control.Isomorphism
44
5+-- Tests if Idris can disambiguate between the three `toVect` operators
6+
57Dec0 : Type -> Type
68Dec0 = Dec
79