git.iko.soy/Idris-dev
on dd71249 help sign in
Idris-dev/test
129 folders, 4 files
../ basic001/Better treatment of unbound implicits 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/Keep type arguments of = when unelaborating 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/Replace 'effects' with neweffects effects002/Replace 'effects' with neweffects error001/Categorise tests error002/Categorise tests error003/Remove dodgy unification hack error004/Make proof arguments to list functions implicit 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/Truncate results in primitives002 test primitives003/Categorise tests proof001/Categorise tests proof002/More efficiency improvements 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/Use a zipper-like proof state quasiquote001/Update tests for rechecking of quasiquotes quasiquote002/Add goal types to quasiquotes. quasiquote003/Update tests for rechecking of quasiquotes quasiquote004/Add tactics "skip" and "fail" 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/Make --nowarnreach the default (for now). reg003/Better treatment of unbound implicits 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/Inline with blocks 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/Inline with blocks 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/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/Better treatment of unbound implicits 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 reg046/Remove dodgy unification hack reg047/New regression test reg048/Fixed bug regarding insertion in SortedMap. Fixes idris-lang/Idris-dev#1394. Solution based on the diagnosis in @sebzim4500s comment. reg049/Reinsert check for constructor/family mismatch. reg050/Add regression test for operators starting with "!" reg051/Store parameters in function types 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/Fix a bug in qsort 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/Inline with blocks unique001/Fix borrowed type check MakefileDisable primitives003 test in LLVM back end READMEAdded IdrisDoc tests mktest.plChange from shebangs with absolute references to using /usr/bin/env runtest.plAdd assert_smaller function