[Agda] Re: about RingSolver

Nils Anders Danielsson nad at cse.gu.se
Thu Jan 28 17:49:41 CET 2016


On 2016-01-28 17:42, Sergei Meshveliani wrote:
> Probably, the term b + b is normalized here according to the
> equations of the domain (universal algebra ?) of XorRingSolver.
> And it is normalized to `false', and this makes it a proof.
> Right?

There is a discussion in the paper that I referenced (Section 4).

-- 
/NAD


More information about the Agda mailing list