git.iko.soy/Idris-dev
on 496cf41 help sign in
496cf41Abstract from everything to make 'with' more magicEdwin Brady 8d83f38Abstract matched terms from goal type in with clauses (like 'magic with' in Agda)Edwin Brady 11dbfc0Correct totality check of f=f, and add regression testEdwin Brady bc3e807Merge pull request #136 from DanielWaterworth/useful_functionsEdwin Brady 28b68fdMerge pull request #135 from DanielWaterworth/masterEdwin Brady 449e292Tweak totality checkerEdwin Brady 906862aFix traversal of size change graphs Fixes issue #134 - new regression test addedEdwin Brady 8d090c0A couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before doing any totality checkingEdwin Brady d087deaAdded a function, 'range', that returns all of the elements of a finite set, in order, in a vectorDaniel Waterworth 34392c9Added a function, 'last', that returns the last element in a finite setDaniel Waterworth f383b59Added zip and unzip definitions for VectDaniel Waterworth bf1c22eMake traverse_ totalEdwin Brady 0a70480Merge branch 'type' of https://github.com/raichoo/Idris-dev into raichoo-typeEdwin Brady 7ef4be9Mark traverse_ partialEdwin Brady 5eac0eeMerge pull request #128 from startling/record-docEdwin Brady 2b30118Merge pull request #130 from startling/alternativeEdwin Brady b88e7f2Merge pull request #133 from ozgurakgun/fix-linesEdwin Brady dd5001fmake TT aware of Set -> Typeraichoo 6f1f358lines isn't wordsOzgur Akgun 811a3cdRewrote 'mapM' and 'mapM_' as 'traverse' and 'traverse_'.startling e75227bWe no longer need MonadPlus, now that we've got Alternative.startling 583c726infixl declaration for (<|>).startling bdef7ec'sequence' and 'sequence_' don't need Monad, either.startling 112f92aDefined (<$) and ($>), analogous to Haskell's (<*) and (*>)startling 4f93ab6You know, 'when' doesn't need Monad either.startling 376b4b5Alternative instances for Maybe and Liststartling 2d17b67"guard" doesn't need MonadPlus, just Alternative.startling 314bcf1Defined Alternative.startling 12f7a82Allow documentation comments for records.startling 55a55ccUpdate display of Set to TypeEdwin Brady 7fefa89PSet -> PTyperaichoo e4da568Take more care when expanding names in nested parameter blocksEdwin Brady 9070208Update CHANGELOGEdwin Brady cc716d7Make 'Type' the type of types instead of Sets ...after mailing list discussionEdwin Brady bdf11e8Better IO + faster compilation by avoiding needless cases in EVAL/APPLYEdwin Brady 01e4d9cBelieve '%assert_total' for coverage checkingEdwin Brady 267f044Improve case compilation by checking most distinct argument firstEdwin Brady ce9fa93Compile to nested if rather than switch for small casesEdwin Brady 47fb39aMerge pull request #122 from LeifW/monoid_instance_for_stringEdwin Brady 19ef940Merge pull request #120 from DanielWaterworth/masterEdwin Brady 686d19dMerge pull request #118 from raichoo/parserEdwin Brady 7245290Some tiny RTS optimisationsEdwin Brady 7e137a9Add a Monoid instance for String.Leif Warner 3b578c9Bugfix, trivial typoDaniel Waterworth c101721Fix Integer matching bugEdwin Brady 441f51dpossible fixes for missing type signature in data declsraichoo ed85b4eerror messages with possible fixesraichoo 6f23ad0Add version requirement for parsecEdwin Brady 2c58ebaFix elaboration of higher order dependent function types Fixes issue #116Edwin Brady 5803d2bRemove reference to W32 (temporarily)Edwin Brady