git.iko.soy/Idris-dev
on eeec833 help sign in
Idris-dev/test
118 folders, 4 files
../ basic001/Fix reg005. basic002/Fix usage in basic002. basic003/Categorise tests basic004/Categorise tests basic005/Categorise tests basic006/Remove implicit qualifier for 'effect' basic007/Return test033 to the original state. basic008/Categorise tests basic009/Add application context to all error messages basic010/Add a timeout. bounded001/Port Haskell's Bounded class buffer001-disabled/Temporarily disable buffer001 test dsl001/Remove | annotation, make Force/Delay implicit dsl002/Remove | annotation, make Force/Delay implicit dsl003/Add pi to overridable syntax in DSL blocks effects001/Make --nowarnreach the default (for now). effects002/Make --nowarnreach the default (for now). error001/Categorise tests error002/Categorise tests error003/Support mixed induction/coinduction with Inf type error004/Coverage checker fix ffi001/Avoid pollution of test case with ANSI codes ffi002/Test updates for executor and type provider update ffi003/Update test to avoid interactive-mode control chars ffi004/Remove reliance on interactive output from test ffi004 ffi005/Distinguish postulate providers and type providers at use site folding001/Tests for tail recursive implementations of foldr folding002/Change type class top level method generation idrisdoc001/Namespaces only containing private members is now correctly considered empty idrisdoc002/Removed test backups and converted tests to pure bash scripts idrisdoc003/Removed test backups and converted tests to pure bash scripts idrisdoc004/Fixed typo idrisdoc005/Removed test backups and converted tests to pure bash scripts idrisdoc006/Updated idrisdoc006 to be more throughly idrisdoc007/Made test resistant to differences among command implementations idrisdoc008/Added IdrisDoc test which verifies inclusion of abstract and public namespace members interactive001/Fix interactive editing and tests interactive002/Improve inference in monadic code interactive003/Fix interactive editing and tests interactive004/Add :refine (:ref) command for refining a hole io001/Remove | annotation, make Force/Delay implicit io002/Categorise tests io003/Remove | annotation, make Force/Delay implicit literate001/Categorise tests primitives001/Categorise tests primitives002/Categorise tests primitives003/Categorise tests proof001/Categorise tests proof002/Update for new unification error messages proof003/Add --nowarnreach to two tests. proof004/Categorise tests proof005/'Reject' cases to default arg substitution tests. proof006/'Reject' cases to default arg substitution tests. proof007/Tests on default args and substitution records001/Make --nowarnreach the default (for now). records002/Rename record002 test to the correct name! records003/Added nested record access syntax reg001/Remove apply from reg001 since it's in the prelude! reg002/Make --nowarnreach the default (for now). reg003/Implicit "module Main" added reg004/Reset test runscripts to mode 0755 reg005/Categorise tests reg006/Fix earlier %assert_total propagation reg007/Support mixed induction/coinduction with Inf type reg009/Reset test runscripts to mode 0755 reg010/Rewrite error printing to use the pretty-printer reg011/Reset test runscripts to mode 0755 reg012/Reset test runscripts to mode 0755 reg013/Reset test runscripts to mode 0755 reg014/Add Prelude.Vect.transpose reg015/Reset test runscripts to mode 0755 reg016/Reset test runscripts to mode 0755 reg017/Reset test runscripts to mode 0755 reg018/Remove stale .ibcs reg019/Reset test runscripts to mode 0755 reg020/Reset test runscripts to mode 0755 reg021/Reset test runscripts to mode 0755 reg022/Reset test runscripts to mode 0755 reg023/Rewrite error printing to use the pretty-printer reg024/Adjust tests to the changed String show instance reg025/Fix usage in reg025. reg026/Unification changes reg027/Unification changes reg028/Update result of reg028 reg029/fix missing tests reg030/Fix reg030. reg031/Make reg031 char-sign-indifferent. reg032/Categorise tests reg033/Fix silly name shadowing bug and add new test reg034/Fix name propagation in error messages reg035/Evaluator bug fix reg036/Fix parameter name propagation reg037/Treat (=) as a special function name. Includes a regression test. reg038/Tweak scoping rules in instance generation reg039/Fix test reg039 and add it to idris.cabal reg040/Rename test reg040 to avoid clash reg041/Fix precedence of application vs arrows in pprint reg042/Add a regression test. reg044/Check that proof steps introduce no new problems reg045/Deal with 'Delay' in case building properly sugar001/Categorise tests sugar002/Categorise tests sugar003/Categorise tests sugar004/Syntax for failures in pattern matching let/<- totality001/Don't try to compile a test that doesn't have `main` totality002/Categorise tests totality003/Add assert_smaller function totality004/Update test for totality warnings totality005/Update for totality warnings totality006/Tweak notion of recoverability in coverage checker totality007/Stop building packages if there are totality mismatches totality008/Find negative occurrences in positivity checker tutorial001/Fix regression with data declarations in where tutorial002/Add tests for tutorial examples tutorial003/Add tests for tutorial examples tutorial004/Add tests for tutorial examples tutorial005/Add tests for tutorial examples tutorial006/Fix name propagation in error messages Makefilefix missing tests READMEAdded IdrisDoc tests mktest.plChange from shebangs with absolute references to using /usr/bin/env runtest.plAdd assert_smaller function