Compare commits

...

2 Commits

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

View File

@ -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

View File

@ -24,7 +24,8 @@ 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
data Tree (l u : Carrier ±) : Set (c ℓ₂) where
leaf : .(l ≤± u) Tree l u
node : (x : Carrier) Tree l [ x ] Tree [ x ] u Tree l u