Sized Types [Re: [Agda] proving termination trouble again]

[Robin Green]

How do sized types compare to defining a function using well-founded
recursion? What are the advantages and disadvantages of the two
approaches?
-- 
Robin