git.iko.soy/Idris-dev
on bfa39bf help sign in
history ofeffects/Effects.idr
all commits
3c32b65Whitespace cleanup.George Leontiev 9b74595Change '!' syntax and semantics to be uniformEdwin Brady 20c71b0Change implicit bind notation to a postfix !Edwin Brady 8c9ec38Added 'implicit bind' syntaxEdwin Brady a9f184dA bit more syntactic sugar for effect testingEdwin Brady 50c66f9Added "if_valid" syntax rule for possibly failing EffectsEdwin Brady 1bc3002Some Eff experimentation, adding a 'test' commandEdwin Brady 70a041fAnother minor efficiency gain in elaboratorEdwin Brady 2311d55rename O into Zraichoo 7bfa10cSome unification fixesEdwin Brady cc7426fFix totality of updateWith/rebuildEnv in EffectsEdwin Brady ea6bb9aMerge branch 'ImprovedReflection' of https://github.com/JanBessai/Idris-dev into JanBessai-ImprovedReflectionEdwin Brady b27ad3eEff note for the future...Edwin Brady b65a0fbInclude reflection of the current goal in proofscript argumentsJan Bessai 6440a7bRepaired effects library, less attacks in applyTacticJan Bessai f31a70bMinor effects changes (locally, search depth)Edwin Brady 9cb4a83Minor effects changes (locally, search depth)Edwin Brady 9724992Minor tinkering with effectsEdwin Brady 8cf25fcAdd runPureEnvEdwin Brady 5593697Rename EFF to EFFECT (for more consistent naming rules)Edwin Brady 0b5a5b3Added effects package and associated testsEdwin Brady