The Effects Tutorial¶
A tutorial on the Effects package in Idris.
Effects and the
There is a new module in the
provides the resource tracking facilities of Effects but with
better support for creating and deleting resources, and implementing
resources in terms of other resources.
Unless you have a particular reason to use Effects you are strongly
recommended to use
Control.ST instead. There is a tutorial available
on this site for
Control.ST with several examples
(用 Idris 实现带有状态的系统：ST 教程).
The documentation for Idris has been published under the Creative Commons CC0 License. As such to the extent possible under law, The Idris Community has waived all copyright and related or neighbouring rights to Documentation for Idris.
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/