git.iko.soy/Idris-dev
on bd89fdc help sign in
Idris-dev/test
20 folders, 4 files
../ reg001/Warn when generating a setter for a record fails ...rather than failing (since it may just not work for dependent records) reg002/Allow forward declaration of data structures To support induction-recursion and mutual data definitions Syntax is as a normal data declaration, but without the 'where' or '=' sections test001/uppercase modulenames test002/More on errors; propagate line numbers test003/uppercase modulenames test004/uppercase modulenames test005/uppercase modulenames test006/uppercase modulenames test007/uppercase modulenames test008/uppercase modulenames test009/uppercase modulenames test010/Add size change termination Now deals with recursive functions (still only simple structural size changes spotted, however) test011/uppercase modulenames test012/uppercase modulenames test013/uppercase modulenames test014/Allow forward declaration of data structures To support induction-recursion and mutual data definitions Syntax is as a normal data declaration, but without the 'where' or '=' sections test015/uppercase modulenames test016/Totality checker improvements Now does a better job of checking type class instances for totality, by inlining dictionaries where possible. Added %default total declarations to some libraries where possible test017/Totality checker improvements Now does a better job of checking type class instances for totality, by inlining dictionaries where possible. Added %default total declarations to some libraries where possible test018/Small change to doc comment syntax (allow spaces before | or ^) MakefileAdded test directory and a single test... READMEAdded raw (non-typesafe) message passing library (System.Concurrency.Raw) mktest.plWarn when generating a setter for a record fails ...rather than failing (since it may just not work for dependent records) runtest.plWarn when generating a setter for a record fails ...rather than failing (since it may just not work for dependent records)