Skip to content

Correct handling of observations in weakestpre - #536

Open
maxvistrup wants to merge 3 commits into
leanprover-community:masterfrom
maxvistrup:master
Open

Correct handling of observations in weakestpre#536
maxvistrup wants to merge 3 commits into
leanprover-community:masterfrom
maxvistrup:master

Conversation

@maxvistrup

Copy link
Copy Markdown

This PR is parallel to the corresponding upstream Iris MR.

This is in preparation for an upcoming PR changing the semantics of prophecy variables, corresponding to this MR in upstream Iris (which I will update soon).

@markusdemedeiros markusdemedeiros added the blocked The issue is blocked by a different issue. label Jul 27, 2026
@markusdemedeiros

Copy link
Copy Markdown
Collaborator

Nice. Let's wait until the MR is accepted upstream.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

blocked The issue is blocked by a different issue.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants