git.iko.soy/Idris-dev
on bf4e535 help sign in
history ofsrc/Idris/Providers.hs
all commits
e1f139aLibrary rearrangement done.David Raymond Christiansen 971d88dAnnotate several top-level functionsMichael Maloney 91bbae7More informative provider errorDavid Raymond Christiansen e5bc47eDistinguish postulate providers and type providers at use siteDavid Raymond Christiansen d3eb486First attempt now at substitution to default argsTimo Petteri Sinnemäki c1ef938New syntax for documentation commentsDavid Raymond Christiansen 5365977Postulate providersDavid Raymond Christiansen ef16e5aWhitespace cleanupDavid Raymond Christiansen fab7083Decorate type provider errors with source locationDavid Raymond Christiansen 803194fArgument options (instead of just a Bool for lazy)Edwin Brady 46e894dUse Data.Text for variable namesEdwin Brady 5000aebAdd a Cabal libraryBrian McKenna 63038b3Use the ErrorT failure functions and attempt to preserve error structureDavid Christiansen a063bfaSome refactoring in CaseOp Separate case trees for totality checking, compile time and run time and lift into their own data structure, so that it's clear which one to use when.Edwin Brady 8eb2087Separate IO and PrimIO PrimIO is the internal primitive, IO is the user version which requires an explicit World token to be passed in which programmers have no access to directly. Fixes #185 and fixes #325Edwin Brady 55ec9cbRemove unused importDavid Christiansen 2bf5a3cClean up implementation of type providersDavid Christiansen 0752bedUpdate type providers so that the decision of failure or otherwise is made in IODavid Christiansen 9af2d93Add type provider errors + test caseDavid Christiansen 879769aExecute type providers while typecheckingDavid Christiansen 0f49abcAdded first steps in type providersDavid Christiansen