diff options
| -rw-r--r-- | Everything.agda | 1 | ||||
| -rw-r--r-- | Examples.agda | 39 |
2 files changed, 40 insertions, 0 deletions
diff --git a/Everything.agda b/Everything.agda index 7399254..e1734a9 100644 --- a/Everything.agda +++ b/Everything.agda @@ -10,3 +10,4 @@ import BFF import Bidir import LiftGet import Precond +import Examples diff --git a/Examples.agda b/Examples.agda new file mode 100644 index 0000000..70628a5 --- /dev/null +++ b/Examples.agda @@ -0,0 +1,39 @@ +module Examples where + +open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_) +open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_) + +import GetTypes +import FreeTheorems + +open GetTypes.VecVec using (Get) +open FreeTheorems.VecVec using (assume-get) + +reverse' : Get +reverse' = assume-get reverse + +double' : Get +double' = assume-get f + where g : ℕ → ℕ + g zero = zero + g (suc n) = suc (suc (g n)) + f : {A : Set} {n : ℕ} → Vec A n → Vec A (g n) + f [] = [] + f (x ∷ v) = x ∷ x ∷ f v + +double'' : Get +double'' = assume-get (λ v → v ++ v) + +take' : ℕ → Get +take' n = assume-get (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) + 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 |