Compare commits

..

No commits in common. "eaae27f04387dcf1b00a829d1750b20b9bc95ded" and "35ca2704765a7276dccc96d722512abccc628408" have entirely different histories.

2 changed files with 4 additions and 5 deletions

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 = })) 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

View File

@ -24,10 +24,9 @@ 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
Heap : Set (c ℓ₂) Heap : Set (c ℓ₂)
Heap = Tree ⊥± ⊤± Heap = Tree ⊥± ⊤±