“General Recursion using Coinductive Monad” Got Right
October 2, 2008
Anton Setzer argued in his letter to the Agda mailing list that we should go back to a category theoretical view of codata, and Dan Doel soon successfully experimented the ideas.
[More ...]
- 0 Comments
Tags: Agda, Dependent Type, Termination.