3 open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_)
4 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_)
9 open GetTypes.VecVec using (Get)
10 open FreeTheorems.VecVec using (assume-get)
13 reverse' = assume-get reverse
16 double' = assume-get f
19 g (suc n) = suc (suc (g n))
20 f : {A : Set} {n : ℕ} → Vec A n → Vec A (g n)
22 f (x ∷ v) = x ∷ x ∷ f v
25 double'' = assume-get (λ v → v ++ v)
28 take' n = assume-get (f n)
29 where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ⊓ n)
32 f (suc n) (x ∷ xs) = x ∷ f n xs
35 drop' n = assume-get (f n)
36 where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ∸ n)
39 f (suc n) (x ∷ xs) = f n xs