git.iko.soy/Idris-dev
on fafe598 help sign in
Idris-dev/test
55 folders, 4 files
../ reg001/rename O into Z reg002/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc reg003/Refactoring of parser to Trifecta, documenting and updating some items/fixing some issues. reg004/rename O into Z reg005/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc reg006/Better representation and rendering of generated names reg007/Fix compilation of unqualified constructor names reg008/rename O into Z reg009/Fix shadowing bug with dependent pair bindings reg010/Indent terms printed in typechecking errors reg011/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc 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/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc reg015/Fix eta problem reg016/javascript: tests should use node with shebang reg017/javascript: tests should use node with shebang reg018/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc reg019/Some unification fixes reg020/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc reg021/Unification fix If f x = g y fails to unify due to f and g failing to unify, record the whole application as failed, otherwise we might accidentally unify x and y. Fixes #409 reg022/Add a 'compute' before elaboration to expand type synonyms etc reg023/Propagate '%assert_total' to with blocks reg024/Propagate '%assert_total' to with blocks test001/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc test002/Refactoring of parser to Trifecta, documenting and updating some items/fixing some issues. test003/javascript: tests should use node with shebang test004/Separate IO and PrimIO PrimIO is the internal primitive, IO is the user version which requires an explicit World token to be passed in which programmers have no access to directly. Fixes #185 and fixes #325 test005/rename O into Z test006/rename O into Z test007/rename fmap to map test008/javascript: tests should use node with shebang test009/javascript: tests should use node with shebang test010/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc test011/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc test012/Proper executable and object file creation via maven + need for run_java tests removed test013/javascript: tests should use node with shebang test014/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc test015/rename O into Z test016/rename O into Z test017/Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc test018/Proper executable and object file creation via maven + need for run_java tests removed test019/rename O into Z test020/Refactoring of parser to Trifecta, documenting and updating some items/fixing some issues. 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/Separate IO and PrimIO PrimIO is the internal primitive, IO is the user version which requires an explicit World token to be passed in which programmers have no access to directly. Fixes #185 and fixes #325 test025/New module chaser, for better dependency checking and rebuilding Now treats each source file separately, building a tree of dependencies, and rebuilding if any dependencies have updated. In particular, this fixes a problem with stale definitions hanging ar… test026/Make test026 more robust test027/javascript: tests should use node with shebang test028/javascript: tests should use node with shebang test029/Try all names in refine to resolve ambiguity Fixes #426 test030/Fix compilation of unqualified constructor names test031/Add parser and tests for parser for error reflection extension MakefileTest LLVM codegen on travis to reduce future breakage READMETry all names in refine to resolve ambiguity Fixes #426 mktest.plInfrastructure for passing of parameters to idris during tests runtest.plruntest.pl revised and cleaned up