Taneb
/
eratosthenes
1
Fork 0
Code Issues 3 Pull Requests Packages Projects Releases Wiki Activity

Compare commits

base: Taneb:35ca2704765a7276dccc96d722512abccc628408
Branches Tags
Taneb:main
..
compare: Taneb:eaae27f04387dcf1b00a829d1750b20b9bc95ded
Branches Tags
Taneb:main

2 Commits
35ca270476 ... eaae27f043

Author SHA1 Message Date
Nathan van Doorn eaae27f043 Make definition of Tree private 2024-07-16 06:18:06 +02:00
Nathan van Doorn 086e98e532 Remove unnecessary public 2024-07-11 21:46:26 +02:00
2 changed files with 5 additions and 4 deletions
Show Stats Expand all files Collapse all files

2
src/Eratosthenes.agda
View File

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

7
src/SplayHeap.agda
View File

@ -24,9 +24,10 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; modu
open import Relation.Nullary.Construct.Add.Extrema open import Relation.Nullary.Construct.Add.Extrema
open import Relation.Nullary.Decidable.Core 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 : Set (c ⊔ ℓ₂)
Heap = Tree ⊥± ⊤± Heap = Tree ⊥± ⊤±