[Agda] proofs for (NON)TERMINATING

[Nils Anders Danielsson]

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.

-- 
/NAD