[Agda] proofs for (NON)TERMINATING

[Nils Anders Danielsson]

On 2018-01-23 19:54, Sergei Meshveliani wrote:
> Please, where it is described the delay monad ?

Venanzio Capretta
General Recursion via Coinductive Types
https://doi.org/10.2168/LMCS-1(2:1)2005

The standard library contains an implementation in
Category.Monad.Partiality. I would not recommend that you use this
implementation. I have another implementation that uses sized types, and
which is therefore in my opinion easier to use (the delay-monad library,
available from http://www.cse.chalmers.se/~nad/software.html). However,
this implementation depends on a different library, which is set up in a
somewhat roundabout way in order to cater to a certain experiment. I
believe others have also implemented the delay monad using sized types.

Here's an example of how one can implement an interpreter for the
untyped λ-calculus using the delay monad:

   http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

-- 
/NAD