git.iko.soy/Idris-dev
on master help sign in
history ofd9516ef..master
compare
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