← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Data/AVL/Sets.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/AVL/Sets.agda
12
12
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
13
13
  where
14
14
 
15
 
open import Category.Functor
16
15
import Data.AVL as AVL
17
16
open import Data.Bool
18
17
open import Data.List as List using (List)
22
21
open import Function
23
22
open import Level
24
23
 
25
 
open RawFunctor (Maybe.functor {f = k ⊔ ℓ})
26
 
 
27
24
-- The set type. (Note that Set is a reserved word.)
28
25
 
29
26
private
48
45
_∈?_ = S._∈?_
49
46
 
50
47
headTail : ⟨Set⟩ → Maybe (Key × ⟨Set⟩)
51
 
headTail s = Prod.map proj₁ id <$> S.headTail s
 
48
headTail s = Maybe.map (Prod.map proj₁ id) (S.headTail s)
52
49
 
53
50
initLast : ⟨Set⟩ → Maybe (⟨Set⟩ × Key)
54
 
initLast s = Prod.map id proj₁ <$> S.initLast s
 
51
initLast s = Maybe.map (Prod.map id proj₁) (S.initLast s)
55
52
 
56
53
fromList : List Key → ⟨Set⟩
57
54
fromList = S.fromList ∘ List.map (λ k → (k , _))