module Records2 where

open import Data.Nat using (ℕ)
open import Records1 hiding (zeros)

-- Use of non-coinductive record in this file works fine:
foo : Derp ℕ ℕ
foo = record { fld1 = 0 ; fld2 = 1 }

-- But uncommenting the identical zeros definition generates an odd error:
-- zeros : Stream ℕ
-- headStr zeros = 0
-- tailStr zeros = zeros

{-
<local-file-path>/Records2.agda:12,1-14
Could not parse the left-hand side headStr zeros
Operators used in the grammar:
  None
when scope checking the left-hand side headStr zeros in the
definition of zeros
-}