[Agda] proofs for (NON)TERMINATING

[Sergei Meshveliani]

On Tue, 2018-01-23 at 15:01 +0100, Nils Anders Danielsson wrote:
> On 2018-01-23 14:14, Sergei Meshveliani wrote:
> > Is it possible to express and prove in Agda the above lemma?
> 
> If you want to prove properties of possibly non-terminating code in
> Agda, then I suggest that you avoid using TERMINATING/NON_TERMINATING
> and instead use one of several methods to represent non-terminating
> computations as total values. One possibility is to use the delay monad.
> 

Please, where it is described the delay monad ?
(I see a certain Monad.agda in Standard library, but do not find the
`delay' word).

------
Sergei