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

[Thorsten Altenkirch]

See Nisse's recent paper:
http://www.cs.nott.ac.uk/~nad/publications/danielsson-productivity.pdf

Thorsten

On 7 Jan 2011, at 16:47, Wolfgang Jeltsch wrote:

> 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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda