[Agda] RingSolver, normalisation

[Andreas Abel]

Hi Christoph,

I cannot load your code in Agda since "Normal" is out of scope.   
However, there could be a trivial error:

> NF : Set
> NF = {p : Polynomial 2} → Normal 2 p
>
> foo : Polynomial 2 → NF
> foo p = normalise p
> -----------------------------
> -- error message
>
> p != .p

If you expand out NF, the type of foo becomes

foo : Polynomial 2 -> {p : Polynomial 2} -> Normal 2 p
foo p {p'} = normalize p

So there are two different p's, did you mean them to be the same?   
Then you need to write

foo : (p : Polynomial 2) -> Normal 2 p
foo p = normalize p

If that does not help, please post your problem again, preferably in a  
form I can immediately load into Agda.

Cheers,
Andreas


Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/