[Agda] Re: problem using "with"

Nils Anders Danielsson nad at chalmers.se
Tue May 15 11:24:52 CEST 2012

On 2012-05-15 11:11, Altenkirch Thorsten wrote:
> The good news is that we know how to implement local case expressions (or
> smart ifs) and I have started this for pisigma. Yes, I know I got stuck on
> this completeness proof but this is not essential for the implementation.

AFAIR your approach was restricted to first-order data. Can you handle
everything now? How inefficient is it?


More information about the Agda mailing list