git.iko.soy/Idris-dev
on fbcd643 help sign in
Idris-dev/test
138 folders, 4 files
../ basic001/Fix use of %flag in test basic001 basic002/Fix usage in basic002. basic003/Categorise tests basic004/Categorise tests basic005/Fixed some tests broken under renaming basic006/Update expected error messages for tests basic007/Return test033 to the original state. basic008/Categorise tests basic009/First renaming attempt basic010/Fixed some tests broken under renaming basic011/Data.Hash library bounded001/Port Haskell's Bounded class buffer001-disabled/Temporarily disable buffer001 test delab001/Fix Curses whitespace issue with test delab001 dsl001/Finished making standard library naming consistent dsl002/Finished making standard library naming consistent dsl003/Finished making standard library naming consistent effects001/Replace 'effects' with neweffects effects002/Fixed some tests broken under renaming error001/Categorise tests error002/Categorise tests error003/Pattern variables should be lifted to top level error004/Fixed some accidentally wrong renamings. Also, adapted some tests to the new names ffi001/Avoid pollution of test case with ANSI codes ffi002/Fixed broken provider test after providing `()` as `Unit` too ffi003/Update test to avoid interactive-mode control chars ffi004/Remove reliance on interactive output from test ffi004 ffi005/Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up 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/First renaming attempt interactive002/Improve inference in monadic code interactive003/Fix interactive editing and tests interactive004/Add :refine (:ref) command for refining a hole interactive005/Support type errors in docstrings interactive006/Allow REPL to run on another port (flag --port) io001/Remove | annotation, make Force/Delay implicit io002/Categorise tests io003/Fixed lack of renaming of `lift` to `Lift` in test literate001/Categorise tests primitives001/Categorise tests primitives002/Add test for new float primitive prim__negFloat primitives003/Finished making standard library naming consistent proof001/First renaming attempt proof002/Fixed some accidentally wrong renamings. Also, adapted some tests to the new names proof003/First renaming attempt proof004/Categorise tests proof005/Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up proof006/Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up proof007/Use a zipper-like proof state quasiquote001/Move Pair/Sigma into Builtins namespace quasiquote002/Add goal types to quasiquotes. quasiquote003/Finished making standard library naming consistent quasiquote004/First renaming attempt records001/Make --nowarnreach the default (for now). records002/Rename record002 test to the correct name! records003/Generate better record projection types reg001/Remove apply from reg001 since it's in the prelude! reg002/Renamed VoidElim to void in order to ensure further consistency reg003/Better treatment of unbound implicits reg004/Reset test runscripts to mode 0755 reg005/Categorise tests reg006/First renaming attempt reg007/First renaming attempt reg009/Fixed some accidentally wrong renamings. Also, adapted some tests to the new names reg010/Update expected error messages for tests reg011/Reset test runscripts to mode 0755 reg012/Renamed VoidElim to void in order to ensure further consistency 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/First renaming attempt reg018/Finished making standard library naming consistent 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/Update expected error messages for tests reg024/Adjust tests to the changed String show instance reg025/Finished making standard library naming consistent reg026/Fixed some accidentally wrong renamings. Also, adapted some tests to the new names reg027/Unification changes reg028/Inline with blocks 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/First renaming attempt reg035/Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up 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/Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up reg042/Add a regression test. reg044/First renaming attempt reg045/Deal with 'Delay' in case building properly reg046/Remove dodgy unification hack reg047/Fixed some accidentally wrong renamings. Also, adapted some tests to the new names reg048/Fixed bug regarding insertion in SortedMap. Fixes idris-lang/Idris-dev#1394. Solution based on the diagnosis in @sebzim4500s comment. reg049/Renamed VoidElim to void in order to ensure further consistency reg050/update test/reg050/expected [2] reg051/Store parameters in function types reg052/Enabled reg052 in travis and update its output reg053/Unification fix for chains of solutions sourceLocation001/A new primitive tactic for getting source locations 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/Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up totality003/Fix a bug in qsort totality004/Update test for totality warnings totality005/Update for totality warnings totality006/Really replaced `lteZero` with `LTEZero` 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/Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up tutorial005/Add tests for tutorial examples tutorial006/Inline with blocks unique001/Really fix output of unique001a... unique002/Don't propagate unique names to 'where' unique003/Fix universe errors, update tests MakefileTake basic011 out of the javascript test suite READMEAdded IdrisDoc tests mktest.plChange from shebangs with absolute references to using /usr/bin/env runtest.plMake tests work with sandboxes