That's what I'm referring to, yes. For more examples of usage you can check Part 2 of https://plfa.github.io/ ====== Georgi -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201123/75e610a8/attachment.html>