Removed return from Effects.
commitce4893244638ba52cdc1662d5da7bbe3594a46ed
authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk>
dateFri 10 Nov 2017, 11:03 (9 years ago)
parent4e5727e
libs/effects/Effects.idr−5
@@ -306,11 +306,6 @@ toEff xs' = id
306306pure : a -> EffM m a xs (\v => xs)
307307pure = Value
308308
309−return : a -> EffM m a xs (\v => xs)
310−return = pure
311−
312−%deprecate Effects.return "Please use `pure`."
313−
314309pureM : (val : a) -> EffM m a (xs val) xs
315310pureM = Value
316311