git.iko.soy/Idris-dev
on bb52ade help sign in
Idris-dev/test
47 folders, 4 files
../ reg001/Make 'Type' the type of types instead of Sets ...after mailing list discussion reg002/javascript: tests should use node with shebang reg003/Make 'Type' the type of types instead of Sets ...after mailing list discussion reg004/javascript: tests should use node with shebang reg005/javascript: tests should use node with shebang reg006/Proper executable and object file creation via maven + need for run_java tests removed reg007/Make sure names are not defined more than once Fixes issue #124 reg008/Changed approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration. reg009/Changed approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration. reg010/Fix error with linearity checking in patterns reg011/Some unification fixes reg012/Added rewrite ... in ... construct rewrite prf in v rewrites the goal type using prf. It is equivalent to applying replace, without the need to provide a predicate. It works by applying the rewrite tactic with prf before elaborating v. reg013/javascript: tests should use node with shebang reg014/Improved type-directed name disambiguation reg015/Fix eta problem reg016/javascript: tests should use node with shebang reg017/javascript: tests should use node with shebang reg018/Check that explicitly given implicit args unify with inferred versions Also exposed a unification bug which unified things which shouldn't be: f x = f y does not imply x = y unless f is injective, and this was not properly checked. reg019/Some unification fixes test001/javascript: tests should use node with shebang test002/Fix error in conversion check Fixes issue #187 test003/javascript: tests should use node with shebang test004/Proper executable and object file creation via maven + need for run_java tests removed test005/javascript: tests should use node with shebang test006/javascript: tests should use node with shebang test007/javascript: tests should use node with shebang test008/javascript: tests should use node with shebang test009/javascript: tests should use node with shebang test010/Proper executable and object file creation via maven + need for run_java tests removed test011/javascript: tests should use node with shebang test012/Proper executable and object file creation via maven + need for run_java tests removed test013/javascript: tests should use node with shebang test014/Check that explicitly given implicit args unify with inferred versions Also exposed a unification bug which unified things which shouldn't be: f x = f y does not imply x = y unless f is injective, and this was not properly checked. test015/javascript: tests should use node with shebang test016/javascript: tests should use node with shebang test017/Proper executable and object file creation via maven + need for run_java tests removed test018/Proper executable and object file creation via maven + need for run_java tests removed test019/javascript: tests should use node with shebang test020/javascript: tests should use node with shebang test021/adapted expected output of test021 to honor modulo test022/Enable alternate names for shared libraries test023/Update type providers so that the decision of failure or otherwise is made in IO test024/Fixed test test025/Fix for proofs in test025 (until I've added support for Decidable.Order) test026/Make test026 more robust test027/javascript: tests should use node with shebang test028/javascript: tests should use node with shebang MakefileCorrect codegen-specific test targets option naming READMEAllow type class constraints in 'using' clauses e.g. if a using block is given as mktest.plInfrastructure for passing of parameters to idris during tests runtest.plInstead of using the installed global idris for tests, pass the PATH to the current compiled one to test and use this