← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Data/Vec/Properties.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (2.1.4 sid)
  • Revision ID: package-import@ubuntu.com-20111129170035-be8cbok8ojft5tjl
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Vec/Properties.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Some Vec-related properties
3
5
------------------------------------------------------------------------
4
6
 
5
 
{-# OPTIONS --universe-polymorphism #-}
6
 
 
7
7
module Data.Vec.Properties where
8
8
 
9
9
open import Algebra
16
16
open import Data.Fin as Fin using (Fin; zero; suc; toℕ; fromℕ)
17
17
open import Data.Fin.Props using (_+′_)
18
18
open import Function
19
 
open import Function.Inverse using (_⇿_)
20
 
open import Level
 
19
open import Function.Inverse using (_↔_)
21
20
open import Relation.Binary
22
21
 
23
22
module UsingVectorEquality {s₁ s₂} (S : Setoid s₁ s₂) where
257
256
 
258
257
-- _[_]=_ can be expressed using lookup and _≡_.
259
258
 
260
 
[]=⇿lookup : ∀ {a n i} {A : Set a} {x} {xs : Vec A n} →
261
 
             xs [ i ]= x ⇿ lookup i xs ≡ x
262
 
[]=⇿lookup {i = i} {x = x} {xs} = record
 
259
[]=↔lookup : ∀ {a n i} {A : Set a} {x} {xs : Vec A n} →
 
260
             xs [ i ]= x ↔ lookup i xs ≡ x
 
261
[]=↔lookup {i = i} {x = x} {xs} = record
263
262
  { to         = PropEq.→-to-⟶ to
264
263
  ; from       = PropEq.→-to-⟶ (from i xs)
265
264
  ; inverse-of = record