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 = ℕ}))
+open import SplayHeap (On.totalOrder ≤-totalOrder (proj₂ {A = ℕ})) public
 
 insertPrime : ℕ → Heap → Heap
 insertPrime p table = insert (p , p * p) table

src/SplayHeap.agda

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