Taneb
/
eratosthenes
1
Fork 0
Code Issues 3 Pull Requests Packages Projects Releases Wiki Activity

Make definition of Tree private

This commit is contained in:
Nathan van Doorn 2024-07-16 06:18:06 +02:00
parent 086e98e532
commit eaae27f043
1 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/SplayHeap.agda
View File

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