test.agda

open import Data.Nat
open import Data.Bool

mutual
  data Stream (A : Set) : Set where
    []ˢ : Stream A
    _∷ˢ_ : A → ∞Stream A → Stream A

  record ∞Stream (A : Set) : Set where
    coinductive
    field
      force : Stream A
open ∞Stream public

even? : ℕ → Bool
even? zero          = true
even? (suc zero)    = false
even? (suc (suc n)) = even? n

step : ℕ → ℕ
step n with even? n
… | true = ⌊ n /2⌋
… | false = 3 * n + 1

collatz : ℕ → Stream ℕ
collatz 1 = 1 ∷ˢ λ where .force → []ˢ
collatz n = n ∷ˢ λ where .force → collatz (step n)