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

sim: (eqs) should frame its internal conseq #703

Open
fdupress opened this issue Feb 5, 2025 · 0 comments
Open

sim: (eqs) should frame its internal conseq #703

fdupress opened this issue Feb 5, 2025 · 0 comments
Labels
enhancement good-to-have

Comments

@fdupress
Copy link
Member

fdupress commented Feb 5, 2025

When using sim with explicit post-condition, the goal generated to show that the stated equalities imply the post is not framed by the pre-condition. This is limiting, but not blocking. (An explicit conseq before sim solves the issue.)

It would be nice for sim to frame its own internal conseq.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement good-to-have
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@fdupress