git.iko.soy/Idris-dev
on 3eabe79 help sign in
3eabe79Added unelaboration definitionEdwin Brady 93ccf9aminor tinkerEdwin Brady 6a8c4e7Some TODO notes and revisions in the paperEdwin Brady 46b7a4eInstall support headers; allow arbitrary types in foreign callsEdwin Brady e7906baAdded support/ directory so that library can use C support filesEdwin Brady 9e399b2Merge pull request #24 from MekeorMelire/masterEdwin Brady a391979Minor paper changesEdwin Brady 20fc41cadded word-function as in haskell in prelude.string.Mekeor Melire b90c3b4added copyright noteMekeor Melire 78fb1dbadded takeWhile and dropWhile to lib/prelude/list.idrMekeor Melire 400f858Add effect_ annotations for better IO behaviourEdwin Brady d9516eftypos againEdwin Brady ce0bc84Fix typosEdwin Brady 20f5db1related work and conclusionEdwin Brady a3569e5Some proofreading, filling in some gaps.Edwin Brady 2c5c768tinkerEdwin Brady 9d389c4AbstractEdwin Brady 2899286An introductionEdwin Brady b01a78eQuick hack at :info for exploring type classesEdwin Brady 8c5ca29Start introEdwin Brady da674d3Elaborating metavariables and caseEdwin Brady 43ffd25Instance tactic explanationEdwin Brady 535d77bAdd --ibcsubdir option (thanks to Dirk Ullrich)Edwin Brady 6c08816More paper changesEdwin Brady 7e248efMerge branch 'master' of github.com:edwinb/Idris-devEdwin Brady 9bb92a5matchWithEdwin Brady 067f4faUtil.Pretty missingEdwin Brady 08797aeFix bug with de-elaboration of sigma typesEdwin Brady 455ae60Attempt to resolve type classes before applicationEdwin Brady e74e08dMore on elaborationEdwin Brady 36abfdaElaborating expressionsEdwin Brady a678b80:t prints all names, rather than checking for unique nameEdwin Brady 2037fe8Change precedence of ++ to be higher than ::Edwin Brady 7b10040TinkerEdwin Brady 78f5e62Primitive tactic descriptionsEdwin Brady 4dfa16bMinor rearrangingEdwin Brady eb2c9f9Small paper updatesEdwin Brady 2b5505dA bit on proof stateEdwin Brady 86c5060An elaboration exampleEdwin Brady 4d2f0feMore on the core TTEdwin Brady 8bf44c2More implementation paperEdwin Brady 0af8a2eWork on implementation paper; tutorial fixesEdwin Brady 8d4a93bMerge pull request #17 from dpmulligan/masterEdwin Brady 5602ea7A small cleanup after missing some stray ends in the diff.Dominic Mulligan 2ba8712Merge branches 'improved-pretty-printing' and 'master'Dominic Mulligan 3541c70Merge remote-tracking branch 'upstream/master'Dominic Mulligan 368fdf6Some playing around with widths to make everything look nicer.Dominic Mulligan c824099Major improvement to pretty printing of proof states, especially when the goal is a large term.Dominic Mulligan dca8f9fNormalise types before applying forcingEdwin Brady a94fd81Remove Eq constraint from NumEdwin Brady