git.iko.soy/Idris-dev
on d90165e help sign in
d90165ecoverage fix for unhandled casesraichoo 2b7db6aFix 'where' lifting bug Make sure functions have unique names when liftedEdwin Brady 379c0f9Added missing test018a.idrEdwin Brady 10a1154Merge pull request #71 from raichoo/masterEdwin Brady bd89fdcSmall change to doc comment syntax (allow spaces before | or ^)Edwin Brady 0b3b0b5Display useful information on :doc (It's ugly though...)Edwin Brady 8e94d86fixed vim indentationraichoo 1ccd94aSyntax for documentation comments and :doc REPL commandEdwin Brady 8464bc4Add field for documentation comments in abstract syntaxEdwin Brady 96f3b9eFix nested parameters blocksEdwin Brady 6d7a6aaChange comment rules Comments cannot begin '{-|' or '--|'. This is now reserved for documentation comments, which will be part of the syntax to support documentation at the REPL.Edwin Brady 2bbea5bTutorial correctionsEdwin Brady 0bfc082Merge pull request #68 from raichoo/libEdwin Brady 319582eElaborate lhs of pattern clause properly in implicit argumentsEdwin Brady 4863bebMerge pull request #67 from raichoo/masterEdwin Brady 29c67e9Pattern matching on strings, big integers and charactersEdwin Brady 8a86c2aflatten for monadsraichoo 2a536ecmoved morphisms to lib/Dataraichoo a52bb30Separate compile time and run time inlinings Run time can be more aggressive - compile time needs to be careful since over aggressive inline can make the termination check harder, especially for type class instances.Edwin Brady 9e58e28Type safe message passing concurrencyEdwin Brady b641ec8Correct cabal fileEdwin Brady 7508b64'par' primitive in builtins (not yet implemented)Edwin Brady c3446b2adjusted date in vimscriptsraichoo 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