diff options
Diffstat (limited to 'Examples.agda')
| -rw-r--r-- | Examples.agda | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/Examples.agda b/Examples.agda index 5971460..25bdbaa 100644 --- a/Examples.agda +++ b/Examples.agda @@ -2,18 +2,21 @@ module Examples where open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_ ; ⌈_/2⌉) open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_) +open import Function using (id) +open import Function.Injection using () renaming (id to id↪) +open import Generic using (≡-to-Π) import GetTypes import FreeTheorems -open GetTypes.VecVec using (Get) -open FreeTheorems.VecVec using (assume-get) +open GetTypes.PartialVecVec using (Get) +open FreeTheorems.PartialVecVec using (assume-get) reverse' : Get -reverse' = assume-get reverse +reverse' = assume-get id↪ (≡-to-Π id) reverse double' : Get -double' = assume-get f +double' = assume-get id↪ (≡-to-Π g) f where g : ℕ → ℕ g zero = zero g (suc n) = suc (suc (g n)) @@ -22,24 +25,24 @@ double' = assume-get f f (x ∷ v) = x ∷ x ∷ f v double'' : Get -double'' = assume-get (λ v → v ++ v) +double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v) take' : ℕ → Get -take' n = assume-get (f n) +take' n = assume-get id↪ (≡-to-Π _) (f n) where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ⊓ n) f n [] = [] f zero (x ∷ xs) = [] f (suc n) (x ∷ xs) = x ∷ f n xs drop' : ℕ → Get -drop' n = assume-get (f n) +drop' n = assume-get id↪ (≡-to-Π _) (f n) where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ∸ n) f zero xs = xs f (suc n) [] = [] f (suc n) (x ∷ xs) = f n xs sieve' : Get -sieve' = assume-get f +sieve' = assume-get id↪ (≡-to-Π _) f where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉ f [] = [] f (x ∷ []) = x ∷ [] |