[Agda] Re: problem using "with"

[Nils Anders Danielsson]

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?

-- 
/NAD