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

[Christoph HERRMANN]

Hi,

I have modified the example akin to the use in Data.Digit (attached)
and this seems to work fine.

However, this still does not provide a normal form
which can be used as a type.

Any ideas how do get that?

Best wishes


On 19 Aug 2010, at 11:24, Christoph HERRMANN wrote:

> Hi again,
> 
> this time I used the operator (= with * on top) which is obviously meant
> for comparing polynomials semantically, omitting the call to normalise
> then, of course. This time, function "checkWorks" passes again and 
> "checkFails" does not explicitly deliver an error but reports unresolved 
> metas, which I assume means that this does not count as a proof.
> 
> Maybe I did something wrong in the way I imported the solver or there
> is a bug in the library. If anyone knows, please tell me as soon as
> possible. The program is attached and the private attribute of the
> operator (= with * on top) in the RIngSolver needs to be removed for that.
> 
> Best Wishes
> 
> <CheckSolver2.agda><ATT00001..txt><ATT00001..txt>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: CheckSolver3.agda
Type: application/octet-stream
Size: 820 bytes
Desc: CheckSolver3.agda
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100819/d4fc457d/CheckSolver3.obj
-------------- next part --------------

--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532