[Agda] Use the ring solver with an abstract ring

[Chantal Keller]

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.

Cheers
Chantal
-------------- next part --------------
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!}