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

Minor Refactorings #74

Open
6 tasks
alxest opened this issue Apr 17, 2021 · 5 comments
Open
6 tasks

Minor Refactorings #74

alxest opened this issue Apr 17, 2021 · 5 comments
Labels
Refactor

Comments

@alxest
Copy link
Collaborator

alxest commented Apr 17, 2021 •
edited
Loading

  • simplify mainpre Type
  • rename SMod -> ModS (parallel with ModL)
  • main_body / mainBody / mainbody
  • main_spec mainspec
  • Give a name to ((flip ModL.get_modsem) skenv)? it is used in Hoare.v and might be frequently used in other places too.
  • The need for Echo2 is somewhat awkward; put APC inside hCallE so that it can be wholly removed?
@alxest
Copy link
Collaborator Author

alxest commented Apr 20, 2021

  • Refactor all examples in the same style

@alxest
Copy link
Collaborator Author

alxest commented Apr 21, 2021

  • Use bimap instead of case

@alxest
Copy link
Collaborator Author

alxest commented Apr 21, 2021

Sim / refines has different direction; align it to src / tgt order.

@alxest
Copy link
Collaborator Author

alxest commented Apr 23, 2021

Sepconj (**) has bad indentation; replace it with some unicode like Iris?

@alxest
Copy link
Collaborator Author

alxest commented Jun 3, 2021

sim_itree -> siml?

@alxest alxest added the Refactor label Jun 3, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Refactor
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@alxest