{-# OPTIONS --guardedness #-}
{-
OPLSS 22 : Introduction to Type Theory
Wednesday Exercises
-}

open import mylib

{-
_*_ : ℕ → ℕ → ℕ
zero * n = 0
suc m * n = m * n + n

fac : ℕ → ℕ
fac zero = 1
fac (suc n) = (suc n) * fac n
-}

{- Define both functions using only the iterator It-ℕ -}


_*-it_ : ℕ → ℕ → ℕ
_*-it_ = {!!}

fac-it : ℕ → ℕ
fac-it = {!!}

{-
from : ℕ → Stream ℕ
head (from n) = n
tail (from n) = from (suc n)

mapS : (A → B) → Stream A → Stream B
head (mapS f as) = f (head as)
tail (mapS f as) = mapS f (tail as)
-}

{-
Define these functions only using CoIt-Stream
-}

from-co : ℕ → Stream ℕ
from-co = {!!}

mapS-co : (A → B) → Stream A → Stream B
mapS-co = {!!}

{-
_+∞_ : ℕ∞ → ℕ∞ → ℕ∞
pred (m +∞ n) with pred m
... | nothing = pred n
... | just m' = just (m' +∞ n)
-}

{-
Define this functions using only CoIt-ℕ
-}

_+∞-co_ : ℕ∞ → ℕ∞ → ℕ∞
_+∞-co_ = {!!}

{-
Define multiplication for conatural numbers
using copattern matching and guarded corecursion.
-}

_*∞_ : ℕ∞ → ℕ∞ → ℕ∞
_*∞_ = {!!}