git.iko.soy/Idris-dev
on fa5a047 help sign in
Idris-dev/test
152 folders, 4 files
../ basic001/Move Fin, Vect and So from prelude to base basic002/Fix usage in basic002. basic003/Categorise tests basic004/Categorise tests basic005/Move Fin, Vect and So from prelude to base basic006/Move Fin, Vect and So from prelude to base basic007/Disable backend-dependent test basic008/Categorise tests basic009/Move Fin, Vect and So from prelude to base basic010/Fixed some tests broken under renaming basic011/Data.Hash library basic012/Support scoped type class constraints bounded001/Port Haskell's Bounded class buffer001-disabled/Temporarily disable buffer001 test delab001/Fix Curses whitespace issue with test delab001 dsl001/Move Fin, Vect and So from prelude to base dsl002/Move Fin, Vect and So from prelude to base dsl003/Move Fin, Vect and So from prelude to base effects001/Fix visibility of imported things effects002/Move Fin, Vect and So from prelude to base effects003/Add missing test file error001/Categorise tests error002/Categorise tests error003/Move Fin, Vect and So from prelude to base error004/Fixed some accidentally wrong renamings. Also, adapted some tests to the new names error005/Move Fin, Vect and So from prelude to base ffi001/New language-dependent FFI ffi002/Fixed broken provider test after providing `()` as `Unit` too ffi003/Update test to avoid interactive-mode control chars ffi004/Primitive type for world state ffi005/Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up folding001/Move Fin, Vect and So from prelude to base folding002/Move Fin, Vect and So from prelude to base 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 idrisdoc009/Fix Curses craziness in test + missing test file interactive001/Move Fin, Vect and So from prelude to base interactive002/Move Fin, Vect and So from prelude to base interactive003/Move Fin, Vect and So from prelude to base interactive004/Move Fin, Vect and So from prelude to base interactive005/Support type errors in docstrings interactive006/Allow REPL to run on another port (flag --port) interactive007/Proper REPL module reloading io001/Remove | annotation, make Force/Delay implicit io002/Categorise tests io003/Fix visibility of imported things literate001/Categorise tests primitives001/Categorise tests primitives002/Add test for new float primitive prim__negFloat primitives003/Move Fin, Vect and So from prelude to base primitives004/Added bit vectors to the C backend proof001/Move Fin, Vect and So from prelude to base proof002/Move Fin, Vect and So from prelude to base proof003/New way of dealing with unmatchable patterns 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/Support scoped type class constraints proof008/"claim" and "unfocus" tactics quasiquote001/Move Pair/Sigma into Builtins namespace quasiquote002/Move Fin, Vect and So from prelude to base quasiquote003/Move Fin, Vect and So from prelude to base quasiquote004/First renaming attempt quasiquote005/Raw quasiquote patterns records001/Move Fin, Vect and So from prelude to base 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/Move Fin, Vect and So from prelude to base reg003/Better treatment of unbound implicits reg004/Reset test runscripts to mode 0755 reg005/Move Fin, Vect and So from prelude to base reg006/First renaming attempt reg007/First renaming attempt reg009/Move Fin, Vect and So from prelude to base reg010/Better typecase check reg011/Move Fin, Vect and So from prelude to base reg012/Move Fin, Vect and So from prelude to base reg013/Reset test runscripts to mode 0755 reg014/Move Fin, Vect and So from prelude to base reg015/Reset test runscripts to mode 0755 reg016/Reset test runscripts to mode 0755 reg017/First renaming attempt reg018/Move Fin, Vect and So from prelude to base reg019/Reset test runscripts to mode 0755 reg020/Move Fin, Vect and So from prelude to base 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/Move Fin, Vect and So from prelude to base reg026/Move Fin, Vect and So from prelude to base reg027/Unification changes reg028/Inline with blocks reg029/fix missing tests reg030/Fix reg030. reg031/Make reg031 char-sign-indifferent. reg032/Categorise tests reg033/Move Fin, Vect and So from prelude to base reg034/Better typecase check reg035/Move Fin, Vect and So from prelude to base 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/Forgot to commit the update test... reg051-disabled/New language-dependent FFI reg052/Enabled reg052 in travis and update its output reg053/Unification fix for chains of solutions reg054/Check for duplicate names in Can't Convert reg055/Better typecase check reg056/Fix checkPossible when unifying bound vars reg057/Allow class constraints to be named reg058/Scoped implicits fix sourceLocation001/Move Fin, Vect and So from prelude to base sugar001/Categorise tests sugar002/Categorise tests sugar003/Categorise tests sugar004/Syntax for failures in pattern matching let/<- sugar005/Better test for @-_-desugaring totality001/Move Fin, Vect and So from prelude to base totality002/Move Fin, Vect and So from prelude to base totality003/Fix a bug in qsort totality004/Update test for totality warnings totality005/Update for totality warnings totality006/Test case that was accidentally accepted before 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/Move Fin, Vect and So from prelude to base unique001/Pair syntax for unique types unique002/Don't propagate unique names to 'where' unique003/Fix universe errors, update tests MakefileDisable backend-dependent test READMEAdded IdrisDoc tests mktest.plChange from shebangs with absolute references to using /usr/bin/env runtest.plMake tests work with sandboxes