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

Move ArmState notation into a separate file #140

Closed
bollu opened this issue Sep 4, 2024 · 1 comment
Closed

Move ArmState notation into a separate file #140

bollu opened this issue Sep 4, 2024 · 1 comment
Assignees
@bollu

Comments

@bollu
Copy link
Collaborator

bollu commented Sep 4, 2024

@bollu developed notation for memory reads and writes in #136, that @pennyannn would like to reuse. We should move the notation out into a separate file to enable reuse across programs.
@bollu bollu mentioned this issue Sep 4, 2024
Merged
@bollu
Copy link
Collaborator Author

bollu commented Sep 19, 2024

This is done now, and lives in https://github.com/leanprover/LNSym/blob/main/Arm/Syntax.lean

@bollu bollu closed this as completed Sep 19, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@bollu bollu

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@bollu