← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/AVL/IndexedMap.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/IndexedMap.agda
15
15
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
16
16
  where
17
17
 
18
 
open import Category.Functor
19
18
import Data.AVL
20
19
open import Data.Bool
21
20
open import Data.List as List using (List)
23
22
open import Function
24
23
open import Level
25
24
 
26
 
open RawFunctor (Maybe.functor {f = i ⊔ k ⊔ v ⊔ ℓ})
27
 
 
28
25
-- Key/value pairs.
29
26
 
30
27
KV : Set (i ⊔ k ⊔ v)
68
65
_∈?_ k = AVL._∈?_ (, k)
69
66
 
70
67
headTail : Map → Maybe (KV × Map)
71
 
headTail m = Prod.map toKV id <$> AVL.headTail m
 
68
headTail m = Maybe.map (Prod.map toKV id) (AVL.headTail m)
72
69
 
73
70
initLast : Map → Maybe (Map × KV)
74
 
initLast m = Prod.map id toKV <$> AVL.initLast m
 
71
initLast m = Maybe.map (Prod.map id toKV) (AVL.initLast m)
75
72
 
76
73
fromList : List KV → Map
77
74
fromList = AVL.fromList ∘ List.map fromKV