[Agda] Totality checking in Agda

Nils Anders Danielsson nad at cse.gu.se
Wed Jan 23 21:25:31 CET 2019


On 23/01/2019 13.26, Henning Basold wrote:
> But you don't refer to sized types, do you?

No, size-change termination:

   https://en.wikipedia.org/wiki/Size-change_termination_principle

-- 
/NAD


More information about the Agda mailing list