[Agda] Totality checking in Agda

[Nils Anders Danielsson]

On 23/01/2019 12.18, Henning Basold wrote:
> The Foetus productivity checker that is described here:
> https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Termin
> ationChecker and in the there linked publication by Andreas Abel.

Agda has for a long time supported more than Foetus: Andreas Abel added
support for some kind of size-change termination.

-- 
/NAD