Trace Monad refactor #664
Merged
Trace Monad refactor #664
Commits on Aug 23, 2023
-
lib/monads: restyle Trace_Monad.thy
This should now be in sync with Nondet_Monad.thy wherever the two files have similar content. Signed-off-by: Corey Lewis <[email protected]>
-
lib/monads: refactor trace monad theories
This splits material out of Trace_Monad and Trace_VCG and into more specific theories, following the same approach and structure as the nondet theories. This commit is mainly focused on definitions and lemmas that also appear in the nondet monad; trace monad concepts are left where they are for now. Signed-off-by: Corey Lewis <[email protected]>
-
lib/monads: split content out into Trace_RG and Trace_No_Trace
Signed-off-by: Corey Lewis <[email protected]>
-
lib/monads: restyle and reorder trace monad files
Signed-off-by: Corey Lewis <[email protected]>
-
lib: update for trace monad refactor
Signed-off-by: Corey Lewis <[email protected]>
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.