[Iris-Club] A question on invariant identifier namespaces

Jeehoon Kang jeehoon.kang at sf.snu.ac.kr
Wed Aug 17 06:49:11 CEST 2016

> Notice that we overloaded the invariant notation depending on whether
there is an \iota or an N in the superscript.

Ah, I see.  I was confused because I couldn't catch the fact that the
notation is overloaded, and that N↑ is (kinda) the interpretation of the
namespace N.  It is also the reason I was confused about the countability.
Thank you for the clarification!

> Furthermore, the N subscript at the viewshift is implicitly closed.

Not sure how do you mean by "closed."  May I ask what does it mean?

> Does this help?

Yes, Thank you a lot!

Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160817/6bd4c4f0/attachment.html>

More information about the Iris-Club mailing list