MetaprogAgda

MetaprogAgda copied to clipboard

The current function `endoFunctorVec` ```agda endoFunctorVec : ∀ {n} → EndoFunctor λ X → Vec X n endoFunctorVec = applicativeEndoFunctor ``` generates the following error Error : ```agda No instance...

shubhamkumar13

This makes the PDF a lot more usable, so maybe others care too? 😄

Blaisorblade

Thanks for this work! Please accept some minor fixes — hope this helps.

Blaisorblade

(the identity and the constant functors are normal). We did cover this in the lecture, but there is no trace for it in the notes, and this is later referenced.

ohad