[Iris-Club] Iris documentation

[Ralf Jung]

Hi Arthur,

> Great! Here's a couple of things that I've noticed:

Thanks for this feedback!

> p26.
> 
> - "Furthermore, we assume that instances named \gamma_State, ... we will
> later discuss how  this assumption is discharged." I don't think this is
> being discussed elsewhere.

Good catch, that's a dead reference.
There is not much to say though, we just use res-alloc to allocate fresh
instances and assume that the names picked at that time are henceforth
globally known.

> p27.
> 
> - "There are no rules related to invariants here. Those rules will be
> discussed later, in §8.2." This sentence appears at the end of 8.2, but
> there's nothing about invariants in there.

Right, that should have been §8.4.

> Here's another one: the definition of except-0 on p21 mentions "Prop"; shouldn't that be something involving "P"?

*oops* that's a case of two LaTeX macros having too similar names.
Indeed it should be P exactly:

  \diamond P := \later False \/ P

If you have any further questions, don't hesitate to contact us.

Kind regards,
Ralf