14
DiffVec : Set → Diffℕ → Set
16
DiffVec : ∀ {ℓ} → Set ℓ → Diffℕ → Set ℓ
15
17
DiffVec A m = ∀ {n} → Vec A n → Vec A (m n)
17
[] : ∀ {A} → DiffVec A 0#
19
[] : ∀ {a} {A : Set a} → DiffVec A 0#
20
_∷_ : ∀ {A n} → A → DiffVec A n → DiffVec A (suc n)
22
_∷_ : ∀ {a} {A : Set a} {n} → A → DiffVec A n → DiffVec A (suc n)
21
23
x ∷ xs = λ k → V._∷_ x (xs k)
23
[_] : ∀ {A} → A → DiffVec A 1#
25
[_] : ∀ {a} {A : Set a} → A → DiffVec A 1#
26
_++_ : ∀ {A m n} → DiffVec A m → DiffVec A n → DiffVec A (m + n)
28
_++_ : ∀ {a} {A : Set a} {m n} →
29
DiffVec A m → DiffVec A n → DiffVec A (m + n)
27
30
xs ++ ys = λ k → xs (ys k)
29
toVec : ∀ {A n} → DiffVec A n → Vec A (toℕ n)
32
toVec : ∀ {a} {A : Set a} {n} → DiffVec A n → Vec A (toℕ n)
32
35
-- fromVec xs is linear in the length of xs.
34
fromVec : ∀ {A n} → Vec A n → DiffVec A (fromℕ n)
37
fromVec : ∀ {a} {A : Set a} {n} → Vec A n → DiffVec A (fromℕ n)
35
38
fromVec xs = λ k → xs ⟨ V._++_ ⟩ k
37
head : ∀ {A n} → DiffVec A (suc n) → A
40
head : ∀ {a} {A : Set a} {n} → DiffVec A (suc n) → A
38
41
head xs = V.head (toVec xs)
40
tail : ∀ {A n} → DiffVec A (suc n) → DiffVec A n
43
tail : ∀ {a} {A : Set a} {n} → DiffVec A (suc n) → DiffVec A n
41
44
tail xs = λ k → V.tail (xs k)
43
take : ∀ {a} m {n} → DiffVec a (fromℕ m + n) → DiffVec a (fromℕ m)
46
take : ∀ {a} {A : Set a} m {n} →
47
DiffVec A (fromℕ m + n) → DiffVec A (fromℕ m)
44
48
take N.zero xs = []
45
49
take (N.suc m) xs = head xs ∷ take m (tail xs)
47
drop : ∀ {a} m {n} → DiffVec a (fromℕ m + n) → DiffVec a n
51
drop : ∀ {a} {A : Set a} m {n} →
52
DiffVec A (fromℕ m + n) → DiffVec A n
48
53
drop N.zero xs = xs
49
54
drop (N.suc m) xs = drop m (tail xs)