[Agda] Selectively capturing variables from the exterior context.(?)

[Apostolis Xekoukoulotakis]

Let us assume that we have parameterized containers,  and we can have
containers withing containers of possibly different parameters. I would
like that the interior container only be able to capture a variable x from
the external container if they have the same parameter.

I could simply define the interior container as a top level function, but
that would make the code less readable. It would also block the ability to
capture variables when we have 3 nested containers where the first and the
third have the same parameters.

I am inclining in using reflection to introduce those restrictions, but
maybe there is an easier way out.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190618/8def78a4/attachment.html>