From eaae27f04387dcf1b00a829d1750b20b9bc95ded Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 16 Jul 2024 06:18:06 +0200 Subject: [PATCH] Make definition of Tree private --- src/SplayHeap.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 ⊥± ⊤±