/usr/share/agda-stdlib/Data/AVL/Sets.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets, based on AVL trees
------------------------------------------------------------------------
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_)
module Data.AVL.Sets
{k ℓ} {Key : Set k} {_<_ : Rel Key ℓ}
(isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
where
open import Category.Functor
import Data.AVL as AVL
open import Data.Bool
open import Data.List as List using (List)
open import Data.Maybe as Maybe
open import Data.Product as Prod using (_×_; _,_; proj₁)
open import Data.Unit
open import Function
open import Level
open RawFunctor (Maybe.functor {f = k ⊔ ℓ})
-- The set type. (Note that Set is a reserved word.)
private
open module S = AVL (const ⊤) isStrictTotalOrder
public using () renaming (Tree to ⟨Set⟩)
-- Repackaged functions.
empty : ⟨Set⟩
empty = S.empty
singleton : Key → ⟨Set⟩
singleton k = S.singleton k _
insert : Key → ⟨Set⟩ → ⟨Set⟩
insert k = S.insert k _
delete : Key → ⟨Set⟩ → ⟨Set⟩
delete = S.delete
_∈?_ : Key → ⟨Set⟩ → Bool
_∈?_ = S._∈?_
headTail : ⟨Set⟩ → Maybe (Key × ⟨Set⟩)
headTail s = Prod.map proj₁ id <$> S.headTail s
initLast : ⟨Set⟩ → Maybe (⟨Set⟩ × Key)
initLast s = Prod.map id proj₁ <$> S.initLast s
fromList : List Key → ⟨Set⟩
fromList = S.fromList ∘ List.map (λ k → (k , _))
toList : ⟨Set⟩ → List Key
toList = List.map proj₁ ∘ S.toList
|