[Agda] Data.Thunk, cofix question

[William Harrison]

Hi,

      I’m having some difficulty grokking the cofix operator from Data.Thunk. Here it is:

  cofix : ∀[ Thunk P ⇒ P ] → ∀[ P ]
  cofix f = f (λ where .force → cofix f)

Does someone have a simple application of it that they could share with me to “unstick” me? For example, how would you define some simple Stream example with it (e.g., 'ones = 1 : ones’ in Haskell)? If an analogous operator could be defined with musical notation, what would it look like? Any tidbits along those lines would be much appreciated.

Thanks!
Bill