[Agda] Data.Thunk, cofix question

[Nils Anders Danielsson]

On 2020-05-11 20:55, William Harrison wrote:
> Thanks again — was/is there a musical notation formulation of cofix?

In the implementation of cofix, how would you ensure that the
corecursive call is guarded? I suppose that you could make this work by
defining a data type that represents the functions that you intend to
use. Instead of (A → A) → A you could have something like

   Data-type-representing-functions-on A guarded → A,

where the index "guarded" ensures that you have at least one occurrence
of ♯ in the expression.

-- 
/NAD