[Agda] dependent catch all?

Nils Anders Danielsson nils.anders.danielsson at gmail.com
Fri May 30 17:01:32 CEST 2008


On Fri, May 30, 2008 at 2:14 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
>
> One way would be to internally expand the cases covered by the catch-all.

I know Ulf had plans to do this, for precisely this reason. Seems
reasonable. One could optimise things by only expanding catch-alls if
they fail to type check.

-- 
/NAD


More information about the Agda mailing list