Compare commits
No commits in common. "eaae27f04387dcf1b00a829d1750b20b9bc95ded" and "35ca2704765a7276dccc96d722512abccc628408" have entirely different histories.
eaae27f043
...
35ca270476
|
@ -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 = ℕ}))
|
open import SplayHeap (On.totalOrder ≤-totalOrder (proj₂ {A = ℕ})) public
|
||||||
|
|
||||||
insertPrime : ℕ → Heap → Heap
|
insertPrime : ℕ → Heap → Heap
|
||||||
insertPrime p table = insert (p , p * p) table
|
insertPrime p table = insert (p , p * p) table
|
||||||
|
|
|
@ -24,8 +24,7 @@ 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
|
||||||
|
|
||||||
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
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue