From 04b7bf8fabf64a2414d64cfb385f6a397da0a0fb Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 10 Feb 2014 15:49:35 +0100
Subject: add sieve to examples

---
 Examples.agda | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/Examples.agda b/Examples.agda
index 70628a5..5971460 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -1,6 +1,6 @@
 module Examples where
 
-open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_)
+open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_ ; ⌈_/2⌉)
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_)
 
 import GetTypes
@@ -37,3 +37,10 @@ drop' n = assume-get (f n)
         f zero    xs       = xs
         f (suc n) []       = []
         f (suc n) (x ∷ xs) = f n xs
+
+sieve' : Get
+sieve' = assume-get f
+  where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
+        f []           = []
+        f (x ∷ [])     = x ∷ []
+        f (x ∷ _ ∷ xs) = x ∷ f xs
-- 
cgit v1.2.3