[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

-- 
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