git.iko.soy/Idris-dev
on cd58dfb help sign in
history oflibs/effects/Effects.idr
all commits
f7f5836Add Effects.runPureEnvaiya000 1381cdbAdd a `runEnv` document commentaiya000 ce48932Removed return from Effects.Jan de Muijnck-Hughes 8a34c86adjust fixities of common operatorsMichael Morgan 06d9db6Use interface instead class or type class in documentations (#3379)(λ _ λ) f754d9cPurify Idris of "return"David Christiansen a854972Small reduction in constraint generationEdwin Brady 7d0fd03Replace EffElem with Data.List.ElemEric Weinstein 39ab37bMerge pull request #2976 from ulidtko/patch-1Edwin Brady 06914a6Prove dropEnv is totalEdwin Brady 773986eAdd some proof hints for SubList in effectsEdwin Brady c6acad2Replace necessary export modifiersEdwin Brady 4e4b7dfMerge branch 'master' of https://github.com/aaronc/Idris-dev into aaronc-masterEdwin Brady 05d24ffremove conflicting fixity declMaxim Ivanov f5457e0Add the "fmap" shortcut <$> to EffMMaxim Ivanov e3e35a5New rules for name visibilityEdwin Brady 68c019aChange export qualifier keywordsEdwin Brady 4d0a065Change "class/instance" keywordsEdwin Brady d36eeeaAdded totality checks to Effects reordering functions and a %assert_total directive for dropEnv where I cannot figure out how to deal with the failing case (which I'm pretty sure is impossible).Aaron Craelius b9f4de7First attempt at getting order-independent Effects working.Aaron Craelius 272efeaAdd *> as a shortcut for do a; b on EffectsLeif Warner 559a903Merge pull request #2715 from cmcl/fix-effect-commentEdwin Brady a35ccd6Update Eff constructors to remove warningsEdwin Brady 7806ff5Fixed comment of Effect type; ordering incorrect and vague.Craig McLaughlin c36a155Remove ugly FIXMEs from Effects.idrEdwin Brady b678d7cChanged scoping rules for unbound implicits.Edwin Brady ed6441aUpdates and FixesJan de Muijnck-Hughes 6b3307aReplace `default tactics search` with the newer `auto`.Leif Warner 3034fb6Remove argument ordering hack in elaboratorEdwin Brady 08af673Correct comment on sigEdwin Brady 7f9fba5Allow adding new effects in Eff programsEdwin Brady c3cdb9cTrying a new Effects apiEdwin Brady 44bdf1dChanged (<$>) to (<*>)Tenor Biel 26cfbe9Scoped implicits fixEdwin Brady 43127b1Move Fin, Vect and So from prelude to baseEdwin Brady 7b5f4aaFix visibility of imported thingsEdwin Brady 28edc0cEliminate with_val by generalizing valueMelvar Chen c0ac681Turn pureM into a functionMelvar Chen 382542aAdd %no_implicit directiveEdwin Brady b54541fFix doc rot on effects.Jan de Muijnck-Hughes ced7733Replace 'effects' with neweffectsEdwin Brady 930f16a"auto" now does proof searchEdwin Brady 9edaf2eMore documentation for runnning effects.Jan de Muijnck-Hughes cc99207Add staticEff/toEffEdwin Brady 6b69961Rename 'effect' to 'call'Edwin Brady e7a35e9Remove implicit qualifier for 'effect'Edwin Brady 5ba96c1Effect handlers should be coveringEdwin Brady 094be98Add an optional depth to 'search' tacticEdwin Brady c2bd084Add laziness to values which aren't evaluated in all branches of a function.bmsherman b283c0dFix some reachability warnings with EffEdwin Brady