MaxZX added

agda · Nov 12, 2024 · 92db749 · 92db749
1 parent 580e6a0
commit 92db749
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/Cubical/Algebra/MaxZX/PolynomialRingZnew.agda b/Cubical/Algebra/MaxZX/PolynomialRingZnew.agda
@@ -1,8 +1,9 @@
 {-# OPTIONS --cubical #-}
 
 -- PolynomialRingZ.agda
-module PolynomialRingZnew where
+module Cubical.Algebra.MaxZX.PolynomialRingZnew where
 
+open import Agda.Primitive
 open import Agda.Primitive.Cubical
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
@@ -23,7 +24,7 @@ open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyList
 open import Cubical.Data.Bool
 open import Cubical.Data.Empty
 open import Cubical.Tactics.CommRingSolver
-open import ExplMaxIdeal
+open import Cubical.Algebra.MaxZX.ExplMaxIdeal
 
 {- record Inspect {A : Set} (x : A) : Set where
   constructor what