[Agda] without-K problem

Nils Anders Danielsson nad at chalmers.se
Tue Jul 31 22:32:25 CEST 2012

On 2012-06-22 00:43, Nils Anders Danielsson wrote:
> * Reconstruct the parameters when applying the check. This sounds like
>   the way to go.

My attempt at implementing parameter reconstruction for --without-K is
available in the darcs repository.


More information about the Agda mailing list