[Agda] Ringsolver seems ok, but how to get NF?

[Nils Anders Danielsson]

On 2010-08-22 23:34, Christoph HERRMANN wrote:
> the aim to let (Normal n p) appear in the type signature of
> particular functions is  to have a certificate that the object
> is really  semantically equivalent to p.

In that case I think you can ignore most of my previous comment.

--
/NAD