Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove FStar.Ghost.Pull #291

Merged
merged 3 commits into from
Jan 7, 2025
Merged

Remove FStar.Ghost.Pull #291

merged 3 commits into from
Jan 7, 2025

Conversation

gebner
Copy link
Contributor

@gebner gebner commented Dec 17, 2024 •
edited
Loading

In order to remove the usage of the pull axiom, we need to redefine the stt_ghost type to be an erased action returning an erased value:

 let stt_ghost a opens pre post =
-  Ghost.erased (act a Ghost opens pre post)
+  Ghost.erased (act (erased a) Ghost opens pre (as_ghost_post post))

@gebner gebner mentioned this pull request Dec 17, 2024
Merged
@gebner gebner force-pushed the gebner_rm_ghost_pull branch from b83caa2 to d9f1a89 Compare January 7, 2025 00:54
@gebner gebner marked this pull request as ready for review January 7, 2025 00:57
@gebner gebner enabled auto-merge January 7, 2025 00:58
@gebner gebner merged commit 899754c into main Jan 7, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@gebner