add intersperse as another example

1 files changed, 15 insertions, 0 deletions

diff --git a/Examples.agda b/Examples.agda
index 764ac0f..c82bcf4 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -56,3 +56,18 @@ sieve' = assume-get id↪ (≡-to-Π _) f
         f []           = []
         f (x ∷ [])     = x ∷ []
         f (x ∷ _ ∷ xs) = x ∷ f xs
+
+intersperse-len : ℕ → ℕ
+intersperse-len zero          = zero
+intersperse-len (suc zero)    = suc zero
+intersperse-len (suc (suc n)) = suc (suc (intersperse-len (suc n)))
+
+intersperse : {A : Set} {n : ℕ} → A → Vec A n → Vec A (intersperse-len n)
+intersperse s []          = []
+intersperse s (x ∷ [])    = x ∷ []
+intersperse s (x ∷ y ∷ v) = x ∷ s ∷ intersperse s (y ∷ v)
+
+intersperse' : Get
+intersperse' = assume-get suc-injection (≡-to-Π intersperse-len) f
+  where f : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A (intersperse-len n)
+        f (s ∷ v)        = intersperse s v