[Agda] red background when trying to define the Fibonacci sequence

[Wolfgang Jeltsch]

Hi,

I just tried to define the Fibonacci sequence as follows:

    fibonaccis : Stream ℕ
    fibonaccis = 0 ∷ ♯ (1 ∷ ♯ zipWith _+_ fibonaccis (tail fibonaccis))

However, the identifier “fibonaccis” gets a red background. How can I
fix this?

Best wishes,
Wolfgang