From af563cc2bf8dfb20b88ad70a1e0fdd1dd3fa5ed1 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Wed, 5 Feb 2014 11:05:29 +0100
Subject: add examples

---
 Examples.agda | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 Examples.agda

(limited to 'Examples.agda')

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
-- 
cgit v1.2.3