-
Notifications
You must be signed in to change notification settings - Fork 106
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.
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
More Nondet Monad improvements #666
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice! I had no idea that we used static_imp_wp
that much..
imports | ||
Nondet_Lemmas | ||
WPSimp | ||
imports |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
when did we start indenting imports? I know the autoindenter likes to do it, but I'm not sure that that's our policy. @lsf37 ?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I noticed that most of the files in nondet
already had indented imports so I decided to go with the autoindenter and make them consistent. I don't know if we have an official policy, but I'd also be happy to go in the opposite direction and make them consistent with the rest of the repository.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We probably shouldn't fight the auto indenter on this. We used to not indent them, but I'd be happy with indented import statements (and I think I have done that a few times myself now)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Other than the import
indentation question, thumbs up from me.
a4bc396
to
d6bf714
Compare
Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
a28e5b7
to
f436f34
Compare
More improvements to Nondet Monad, following on from #665. In general this improves style and some proofs, removes duplicate lemmas, and stays in sync with coming changes to Trace Monad.