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

field_compatible0_Tarray_offset #700

Closed
andrew-appel opened this issue Jul 21, 2023 · 0 comments · Fixed by #711
Closed

field_compatible0_Tarray_offset #700

andrew-appel opened this issue Jul 21, 2023 · 0 comments · Fixed by #711

Comments

@andrew-appel
Copy link
Collaborator

In the lemma field_compatible0_Tarray_offset, the premise naturally_aligned t is totally unnecessary, it's not even used in the proof. And it's harmful, because it prevents this lemma from being use on arrays of int_or_ptr_type.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix issues #700 and #702 PrincetonUniversity/VST
1 participant
@andrew-appel