Update to stdlib 2.4

eratosthenes.agda-lib

@@ -1,3 +1,3 @@
 name: eratosthenes
 include: src
-depend: standard-library-2.1
+depend: standard-library-2.4

src/Eratosthenes.agda

@@ -10,7 +10,7 @@ module Eratosthenes where
 
 open import Data.Nat.Base
 open import Data.Nat.Induction using (<-wellFounded-fast)
-open import Data.Nat.Properties hiding (≤-total; ≤-isTotalOrder; ≤-totalOrder)
+open import Data.Nat.Properties
 open import Data.List.Base hiding (upTo)
 open import Data.Product.Base
 open import Data.Sum.Base using (inj₁; inj₂)
@@ -27,24 +27,6 @@ open import Relation.Nullary.Decidable
 -- Reimplementations of a couple of things from stdlib because
 -- their existing definitions at time of writing are slow
 
--- ≤-total is currently defined in stdlib using unary arithmetic. This makes it
--- terrible to use as a conditional. Our heap implementation is generic over a
--- total order, so we redefine this and the bundle we care ultimately care
--- about.
-≤-total : Total _≤_
-≤-total m n with m ≤? n
-... | yes m≤n = inj₁ m≤n
-... | no m≰n = inj₂ (≰⇒≥ m≰n)
-
-≤-isTotalOrder : IsTotalOrder _≡_ _≤_
-≤-isTotalOrder = record
-  { isPartialOrder = ≤-isPartialOrder
-  ; total = ≤-total
-  }
-
-≤-totalOrder : TotalOrder _ _ _
-≤-totalOrder = record { isTotalOrder = ≤-isTotalOrder }
-
 -- upTo in stdlib creates larger and larger closures. This causes some slowdown.
 -- We implement it in a tail recursive manner instead.
 upFromThen : ℕ → ℕ → List ℕ
@@ -54,7 +36,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
+private
-  leaf : .(l ≤± u) → Tree l u
+  data Tree (l u : Carrier ±) : Set (c ⊔ ℓ₂) where
-  node : (x : Carrier) → Tree l [ x ] → Tree [ x ] u → Tree l u
+    leaf : .(l ≤± u) → Tree l u
+    node : (x : Carrier) → Tree l [ x ] → Tree [ x ] u → Tree l u
 
 Heap : Set (c ⊔ ℓ₂)
 Heap = Tree ⊥± ⊤±