← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/List/Countdown.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-05-27 19:29:25 UTC
  • mfrom: (8.1.1 experimental)
  • Revision ID: package-import@ubuntu.com-20130527192925-q2tadfousmn0xeav
Tags: 0.7-2
Upload to unstable 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/List/Countdown.agda
125
125
  thick-injective {suc n} (suc i)  zero    zero    _ = refl
126
126
  thick-injective {suc n} (suc i)  zero    (suc k) ()
127
127
  thick-injective {suc n} (suc i)  (suc j) zero    ()
128
 
  thick-injective {suc n} (suc i)  (suc j) (suc k) eq =
129
 
    cong suc $ thick-injective i j k (drop-suc eq)
 
128
  thick-injective {suc n} (suc i)  (suc j) (suc k) {i≢j} {i≢k} eq =
 
129
    cong suc $ thick-injective i j k {i≢j ∘ cong suc} {i≢k ∘ cong suc} (drop-suc eq)
130
130
 
131
131
------------------------------------------------------------------------
132
132
-- The countdown data structure