git.iko.soy/Idris-dev
on ca684b6 help sign in
ca684b6Fix pToV scoping bugEdwin Brady f91a45aMerge branch 'master' of github.com:edwinb/Idris-devEdwin Brady 1a86305Make believe_me abstractEdwin Brady 83fdb4dMerge pull request #73 from raichoo/libEdwin Brady d530abeMerge pull request #80 from raichoo/fixEdwin Brady 718a040Add reg003 testsEdwin Brady aa0693eDisambiguate catch explicitly in CodegenCommonEdwin Brady f855d0fFix a few missing module referencesBenjamin Saunders 6398a7eAdd argument passing to new testsBenjamin Saunders f50f006Expand backend control options and infrastructureBenjamin Saunders 2c6ad9bInfrastructure for passing of parameters to idris during testsBenjamin Saunders 96db606Cleaner data constructor argument pointer storage in RTSBenjamin Saunders f9a1dabFix pattern variable problem when patterns generated by unificationEdwin Brady d90165ecoverage fix for unhandled casesraichoo 27df3e0extended morphisms/categories/arrowsraichoo 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