diff --git a/src/SplayHeap.agda b/src/SplayHeap.agda index 3536350..964fcd2 100644 --- a/src/SplayHeap.agda +++ b/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 - leaf : .(l ≤± u) → Tree l u - node : (x : Carrier) → Tree l [ x ] → Tree [ x ] u → Tree l u +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 Heap : Set (c ⊔ ℓ₂) Heap = Tree ⊥± ⊤±