make one example more meaningful

agda · Aug 2, 2024 · 49ab241 · 49ab241
1 parent 1e251b8
commit 49ab241
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Tactics/CommRingSolver/Examples.agda b/Cubical/Tactics/CommRingSolver/Examples.agda
@@ -65,7 +65,7 @@ module Test (R : CommRing ℓ) (x y z : fst R) where
   ex1 : x ≡ x
   ex1 = solve! R
 
-  ex2 : x ≡ x
+  ex2 : (0r - 1r) · x ≡ 0r - x
   ex2 = solve! R
 
   ex3 : x + y ≡ y + x