on d7e4bfa help sign in
Idris-dev/test
109 folders, 4 files
../ basic001/Fix reg005. basic002/Fix usage in basic002. basic003/Categorise tests basic004/Categorise tests basic005/Categorise tests basic006/Update test for more informative error messages basic007/Return test033 to the original state. basic008/Categorise tests basic009/Add application context to all error messages 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 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/Control whether provider decls accept postulates folding001/Tests for tail recursive implementations of foldr folding002/Tests for tail recursive implementations of foldr idrisdoc001/Removed test backups and converted tests to pure bash scripts idrisdoc002/Removed test backups and converted tests to pure bash scripts idrisdoc003/Removed test backups and converted tests to pure bash scripts idrisdoc004/Removed test backups and converted tests to pure bash scripts idrisdoc005/Removed test backups and converted tests to pure bash scripts idrisdoc006/Removed test backups and converted tests to pure bash scripts idrisdoc007/Made test resistant to differences among command implementations interactive001/Categorise tests interactive002/Improve inference in monadic code interactive003/Proof search fix 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). 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 reg008/Reset test runscripts to mode 0755 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/Reset test runscripts to mode 0755 reg015/Reset test runscripts to mode 0755 reg016/Reset test runscripts to mode 0755 reg017/Reset test runscripts to mode 0755 reg018/Change guardedness check for new-style coinduction 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/fixes reg029 to not use set -u (which does not exist on macosx) reg030/Fix bug in 'forget' for well-typed terms reg031/Make reg031 char-sign-indifferent. reg032/Categorise tests reg033/Fix silly name shadowing bug and add new test reg034/Add application context to all 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/Improve the portability of reg041 sugar001/Categorise tests sugar002/Categorise tests sugar003/Categorise tests sugar004/Syntax for failures in pattern matching let/<- totality001/Categorise tests totality002/Categorise tests totality003/Add assert_smaller function totality004/Change guardedness check for new-style coinduction totality005/Finish guardedness check totality006/Tweak notion of recoverability in coverage 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/Add tests for tutorial examples Makefilejavascript: make folding002 pass READMEAdded IdrisDoc tests mktest.plChange from shebangs with absolute references to using /usr/bin/env runtest.plAdd assert_smaller function