← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to README/AVL.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
README/AVL.agda
30
30
 
31
31
-- Some values.
32
32
 
33
 
v₁ = "cepa" ∷ []
34
 
v₂ = "apa" ∷ "bepa" ∷ []
 
33
v₁  = "cepa" ∷ []
 
34
v₁′ = "depa" ∷ []
 
35
v₂  = "apa" ∷ "bepa" ∷ []
35
36
 
36
37
-- Empty and singleton trees.
37
38
 
45
46
 
46
47
t₂ = insert 1 v₁ t₁
47
48
 
 
49
-- If you insert a key-value pair and the key already exists in the
 
50
-- tree, then the old value is thrown away.
 
51
 
 
52
t₂′ = insert 1 v₁′ t₂
 
53
 
48
54
-- Deletion of the mapping for a certain key.
49
55
 
50
56
t₃ = delete 2 t₂
88
94
q₅ : toList t₂ ≡ (1 , v₁) ∷ (2 , v₂) ∷ []
89
95
q₅ = refl
90
96
 
 
97
q₅′ : toList t₂′ ≡ (1 , v₁′) ∷ (2 , v₂) ∷ []
 
98
q₅′ = refl
 
99
 
91
100
------------------------------------------------------------------------
92
101
-- Views
93
102