← Back to branch summary

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

« back to all changes in this revision

Viewing changes to README/AVL.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:
README/AVL.agda
103
103
-- Partitioning a tree into the smallest element plus the rest, or the
104
104
-- largest element plus the rest.
105
105
 
106
 
open import Category.Functor using (module RawFunctor)
107
106
open import Function using (id)
108
 
import Level
109
 
 
110
 
open RawFunctor (Maybe.functor {f = Level.zero}) using (_<$>_)
111
107
 
112
108
v₆ : headTail t₀ ≡ nothing
113
109
v₆ = refl
114
110
 
115
 
v₇ : Prod.map id toList <$> headTail t₂ ≡
 
111
v₇ : Maybe.map (Prod.map id toList) (headTail t₂) ≡
116
112
     just ((1 , v₁) , ((2 , v₂) ∷ []))
117
113
v₇ = refl
118
114
 
119
115
v₈ : initLast t₀ ≡ nothing
120
116
v₈ = refl
121
117
 
122
 
v₉ : Prod.map toList id <$> initLast t₄ ≡
 
118
v₉ : Maybe.map (Prod.map toList id) (initLast t₄) ≡
123
119
     just (((1 , v₁) ∷ []) ,′ (2 , v₂))
124
120
v₉ = refl
125
121