[Agda] Question about colists, musical notation vs coinductive records, and all that

[Nils Anders Danielsson]

On 2020-05-03 16:59, William Harrison wrote:
> The phrase “λ where .force → …” effectively plays the role of ‘freeze’
> in conventional presentations of thunks while passing .force (e.g.,
> “xs .force”) is effectively ’thaw’. Is that right?

I think it makes sense to think of these constructions in this way.

-- 
/NAD