[Agda] Use the ring solver with an abstract ring

[Andreas Abel]

I don't know, but at least you should instantiate the RingSolver module 
to its parameters:

 > open import Algebra.RingSolver

should be

 > open import Algebra.RingSolver CoefficientRing R embedding decide

for some suitable definitions of CoefficientRing, embedding, and decide.

Maybe the CoefficientRing could be the integers?

Best,
Andreas

On 18.10.2017 16:51, Chantal Keller wrote:
> Hi
> 
> How can I use the ring solver with an abstract ring?
> 
> See the attached file for an example of what I would like to do.
 >
 > open import Algebra
 > open import Algebra.RingSolver.AlmostCommutativeRing
 >
 > module sr {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂) where
 >
 > open AlmostCommutativeRing R
 > open import Algebra.RingSolver
 >
 >
 >
 >
 > foo : (n : Carrier) → n ≈ n + 0#
 > foo n = {!solve 1!}

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/