Make definition of Tree private

src/Eratosthenes.agda

@@ -54,7 +54,7 @@ upFromThen from (suc then) = from ∷ upFromThen (suc from) then
 upTo : ℕ → List ℕ
 upTo = upFromThen 0
 
-open import SplayHeap (On.totalOrder ≤-totalOrder (proj₂ {A = ℕ})) public
+open import SplayHeap (On.totalOrder ≤-totalOrder (proj₂ {A = ℕ}))
 
 insertPrime : ℕ → Heap → Heap
 insertPrime p table = insert (p , p * p) table

src/SplayHeap.agda

@@ -24,9 +24,10 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; modu
 open import Relation.Nullary.Construct.Add.Extrema
 open import Relation.Nullary.Decidable.Core
 
-data Tree (l u : Carrier ±) : Set (c ⊔ ℓ₂) where
-  leaf : .(l ≤± u) → Tree l u
-  node : (x : Carrier) → Tree l [ x ] → Tree [ x ] u → Tree l u
+private
+  data Tree (l u : Carrier ±) : Set (c ⊔ ℓ₂) where
+    leaf : .(l ≤± u) → Tree l u
+    node : (x : Carrier) → Tree l [ x ] → Tree [ x ] u → Tree l u
 
 Heap : Set (c ⊔ ℓ₂)
 Heap = Tree ⊥± ⊤±