diff options
| -rw-r--r-- | Examples.agda | 15 |
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 |