I agree with BSD3 license for all my contributions.

As the title mentions wp_cas_suc fails with total weakest precondition. The reason seems to be that the well-formedness assumption on what is stored at the location is not discharged correctly since I can make it go through with
`wp_apply (twp_cas_suc with "Hpt"); [by left | ].`

instead of wp_cas_suc.

See the attached file for a complete example.

**Aleš Bizjak**
(53de53db)
*
at
02 Nov 09:25
*

Make the README correspond to the updated paper.

@robbertkrebbers I would guess it is this construction https://ncatlab.org/nlab/show/adjoint+monad This requires that the comonad preserves limits (intersections in this case) though. In both of these cases you seem to be mimicking the construction of left adjoints (specialized to posets) to a given function.

@sfs
Your definition of `<int>`

above does not, in general, commute with existentials.
If you take your monoid of resources to be the interval [0,1] with + as the
operation your definition would give
`<int>y(q) = ∅`

for `q > 0`

(where y(q) is the set of all p such that `p ≥ q`

).
But `⋃_{q > 0}y(q) = (0,1] `

and `<int>(0,1] = (0,1]`

by your definition.

In my "On Models of Higher-Order Separation Logic" paper with Lars we have investigated the box modality (in the setting of intuitionistic separation logic). We have completely characterized the situation if we require it to preserve intersections. If not, then the largest one (modulo some mild restrictions on the monoid) is the one defined in Section 3 of the paper (although the statement and proof of this did not make it into the paper since it was rather combinatorial). Most of the development in that paper is constructive so should apply to CMRAs as well

@jung Can you point me to models where `True = ∃ x, x ↦ 0`

? I was playing around with one where this was the case. It did not support implication though.

@jung A frame is the same thing as a complete Heyting algebra. But a frame morphism is as you say, not the same thing as a Heyting algebra homomorphism, i.e., it does not preserve implication or arbitrary conjunctions.

I was commenting on the fact that you said that frames only have finite conjunctions, which is not true. But frame morphisms are not required to preserve the additional implied structure, as you correctly say.

@jung I just happened to notice this. Note that frames are the same thing as complete Heyting algebras. In particular they have arbitrary infima because they have arbitrary suprema.

May I ask who is Steven?

What is vprop and what is later_false_em?

FWIW I don't think saying that you can derive Lob from intro makes sense as such (the identity modality has an equivalent introduction rule). You crucially need the existence of fixed points (here you used that contractive functions have fixed points, and that guarding recursive occurrences by later gives a contractive function), which in this case crucially uses the specific model.

Adds more of the examples from the iris lecture notes (and some additional ones).

**Aleš Bizjak**
(a66aa086)
*
at
24 Apr 11:46
*

Merge branch 'ales/lecture-notes-examples' into 'master'

*
... and
1 more commit
*

Adds more of the examples from the iris lecture notes (and some additional ones).

**Aleš Bizjak**
(955aa2d2)
*
at
23 Apr 14:28
*

Add more examples from the lecture notes.

**Aleš Bizjak**
(e146b872)
*
at
23 Apr 14:20
*