[Agda] RingSolver, normalisation

[Christoph HERRMANN]

Hi Andreas,

thank you for your hint. It was
----
NF : {p : Polynomial 2} → Set
NF {p} = Normal 2 p

foo : (p : Polynomial 2) → NF {p}
foo p = normalise p
---
what I meant. *Normal* is the type from the RingSolver
and I have removed the private declaration there as
well.

I think one should export the normalisation because
if you want to compare polynomials it is more convenient
to just compare the normal forms instead of reifying them
first.

Best wishes

On 17 Aug 2010, at 11:49, Andreas Abel wrote:

> 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/
> 

--
 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