git.iko.soy/Idris-dev
on 489ea6f help sign in
489ea6fPass pattern variable names to match compilerEdwin Brady 602ce01Merge branch 'master' of github.com:edwinb/Idris-devEdwin Brady a706b8eProof read for voice/consistencyEdwin Brady 96031d1Normalise rewrite rule so that they apply more easilyEdwin Brady dcb9ca0Change meaning of alternative syntax (| a , b , ... |) Now takes the first alternative to elaborate,rather than requiring exactly one to work. Old behaviour reserved for disambiguating namespaces.Edwin Brady 923e19apaper updatesEdwin Brady f23f336Note on performance and compilationEdwin Brady 32aeb5aDescribe elaboration propertiesEdwin Brady 4d1bd2dElab propertiesEdwin Brady 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