module CheckSolver2 where

open import Data.Bool
open import Data.Unit
open import Data.Fin renaming ( zero to fzero ; suc to fsuc )
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product

import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
open Solver (ACR.fromCommutativeSemiring commutativeSemiring) 

Ex : Set
Ex = Polynomial 2 

vM : Ex
vM = var fzero

vN : Ex
vN = var (fsuc fzero)

foo : Ex → Ex → Ex
foo m n = m :+ n 

checkWorks : ((foo (con 1) vN) ≛ ((con 1) :+ vN)) → Set  
checkWorks _ = ⊤

checkFails : (((con 0) :+ (con 1)) ≛ ((con 1) :+ (con 0))) → Set 
checkFails _ = ⊤