effects Porting the Idris Effects library to Agda. Work in progress. References Edwin Brady, Resource-Dependent Algebraic Effects, TFP 2014