git.iko.soy/Idris-dev
on 2fb2445 help sign in
2fb2445indent proof blocks by 2 spacesraichoo b0ce16cimproved {[( handlingraichoo 53024f8vim mutual blocksraichoo af66f25Added 'mutual' blocks Effect is to elaborate all types in the block before elaborating definitionsEdwin Brady 264b67fMore restrictive automated addition of implicit arguments Only added automatically if they begin with a lower case letter, or appear in a using block. Apologies for breaking code: however, this catches a common class of error which causes confusing (but correct) typechecker behaviour.Edwin Brady 895b323Allow 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 '=' sectionsEdwin Brady 20030b5Merge pull request #65 from raichoo/masterEdwin Brady e3aeee9Merge pull request #64 from dagit/masterEdwin Brady d037f7dfix compile warning on gcc 7.2.1raichoo bba84d5Added raw (non-typesafe) message passing library (System.Concurrency.Raw)Edwin Brady ba6042fMessage passing fixes; also abstract SETTY/GETTY in rtsEdwin Brady 5d2ff60Merge pull request #63 from raichoo/masterEdwin Brady b8fc54etravisci: run test suiteJason Dagit 5da2f7btravis-ci: lower case Haskell to see if that helps with build problemsJason Dagit 592d6c0Add a note about editing config.mkJason Dagit 3bfe418Refactor the makefile so that all the pertinent variables are in config.mkJason Dagit 3e74a93fixed monad module (uppercase)raichoo 671d39aFix name clashes between holes and bound variablesEdwin Brady 74cd49eMinor tutorial updatesEdwin Brady 7438e0fDocument --warnpartial Behaviour fixed so that it doesn't report declared partial functionsEdwin Brady 2541a16No need to store original patternsEdwin Brady 9d53533Correct case of Main in tutorialEdwin Brady 665676bAdded :l and :m commands to REPLEdwin Brady 3f6fd87Bring tutorial up to date with new termination checkerEdwin Brady 9b9d316Add lower bound for HaskelineEdwin Brady 53eb552Merge pull request #62 from dagit/masterEdwin Brady 71a3efaLibrary now builds with "--total"Edwin Brady e11da78Add travis.yml fileJason Dagit 15fc297Merge branch 'master' of https://github.com/edwinb/Idris-devJason Dagit 77a2cd8add vim temp files and cabal-dev directory to git ignoreJason Dagit a41fe5bUse strict StateTJason Dagit 9affb75Totality 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 possibleEdwin Brady f8920a0Deal with higher order recursive arguments in size change graphsEdwin Brady 54ad219Add size change termination Now deals with recursive functions (still only simple structural size changes spotted, however)Edwin Brady ebb75fbCalculate size change graphsEdwin Brady 1d125cfFix test016Edwin Brady 991ee91Merge branch 'lib' of https://github.com/raichoo/Idris-devEdwin Brady d27925cMerge branch 'master' of https://github.com/raichoo/Idris-devEdwin Brady cad5efbMerge pull request #61 from raichoo/vimcodataEdwin Brady da79b2cvim color adjustmentraichoo ad89090vim default directiveraichoo a76852cvim partial keywordraichoo e49241dvim codata supportraichoo 5c9a88auppercase modulenamesraichoo bf8685eSeparate "productive" and "total" in totality checker Productive can call Total, but not vice versa. This is still a temporary solution - don't rely on anything yet!Edwin Brady dc01a56added 'parameters' support to vimscriptsraichoo 30e4ed8Added simple productivity checker for coinductive definitions Recursive calls must be an argument to a coinductive constructorEdwin Brady 5692e48Added "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time.Edwin Brady 0fd9a47Added regression test for missing cases bugEdwin Brady 36aa92bReinstate old coverage checker (because it's better...)Edwin Brady