[Agda] dependent catch all?

[Samuel Bronson]

> 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.

Sweet! This would be really handy...