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

[Nils Anders Danielsson]

On 2010-01-18 23:21, Andreas Abel wrote:
> Recursion is then done on the proof of wellfoundedness, an how to
> erase these proofs during compilation is an open issue.

It seems as if Edwin Brady et al. have found a good way to erase
accessibility predicates. See Section 7.3 of "Inductive Families Need
Not Store Their Indices":

  http://www.e-pig.org/downloads/indfam.pdf

--
/NAD