From 086e98e53266d22543a5f5121bbe35c9b4c2c05f Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Thu, 11 Jul 2024 21:46:26 +0200 Subject: [PATCH] Remove unnecessary public --- src/Eratosthenes.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Eratosthenes.agda b/src/Eratosthenes.agda index 0ef1dc3..f8c48c7 100644 --- a/src/Eratosthenes.agda +++ b/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