mention a limitation

agda · Feb 7, 2024 · 036ada4 · 036ada4
1 parent d6cf2a4
commit 036ada4
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/Cubical/Tactics/CommRingSolver/Examples.agda b/Cubical/Tactics/CommRingSolver/Examples.agda
@@ -35,8 +35,15 @@ module TestErrors (R : CommRing ℓ) where
 module TestWithℤ where
   open CommRingStr (ℤCommRing .snd)
 
+{-
+  the following is not possible yet: the ring solver normalises the goal
+  and expands some of the definitions of the operations. A possible fix could be
+  to not normalize - but then one has to (at least) translate every use of a binary
+  minus. (#1101)
+
   ex13 : (x y : ℤ) → (x · y) · 1r ≡ 1r · (y · x)
   ex13 x y = solve! ℤCommRing
+-}
 
   ex0 : (a b : fst ℤCommRing) → a + b ≡ b + a
   ex0 a b = solve! ℤCommRing

diff --git a/Cubical/Tactics/CommRingSolver/Reflection.agda b/Cubical/Tactics/CommRingSolver/Reflection.agda
@@ -13,7 +13,7 @@ open import Cubical.Data.Maybe
 open import Cubical.Data.Sigma
 open import Cubical.Data.List
 open import Cubical.Data.Nat.Literals
-open import Cubical.Data.Int.Base hiding (abs)
+open import Cubical.Data.Int.Base hiding (abs; _-_)
 open import Cubical.Data.Int using (fromNegℤ; fromNatℤ)
 open import Cubical.Data.Nat using (ℕ; discreteℕ) renaming (_+_ to _+ℕ_)
 open import Cubical.Data.Bool