module Records1 where

open import Data.Nat using (ℕ)

record Stream {ℓ} (A : Set ℓ) : Set ℓ where
  coinductive
  field headStr : A
        tailStr : Stream A
open Stream; S = Stream

zeros : Stream ℕ
headStr zeros = 0
tailStr zeros = zeros

record Derp (A B : Set) : Set where
  field
    fld1 : A
    fld2 : B