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

Monads: refactor reader_option and nondet connection #722

Merged
merged 3 commits into from
Mar 1, 2024
Merged

Monads: refactor reader_option and nondet connection #722

merged 3 commits into from
Mar 1, 2024

Commits on Mar 1, 2024

  1. lib/monads: refactor reader_option and nondet connection 

    This reverses the dependency between reader_option and nondet. The
reader_option directory now only contains definitions and lemmas for the
reader_option monad and there's a file in nondet that has the lemmas
connecting the two monads.

In addition to resulting in a more structured divide between the
reader_option and nondet monad, it also makes it possible to setup
reader_option for use with other monads, such as the trace monad.

Signed-off-by: Corey Lewis <[email protected]>
    @corlewis
    corlewis committed Mar 1, 2024
    Configuration menu
    Copy the full SHA
    6166731 View commit details
    Browse the repository at this point in the history

  2. lib+spec+proof+tools: update for reader_option refactor 

    Signed-off-by: Corey Lewis <[email protected]>
    @corlewis
    corlewis committed Mar 1, 2024
    Configuration menu
    Copy the full SHA
    ba42deb View commit details
    Browse the repository at this point in the history

  3. lib/monads/trace: add connection to reader_option 

    This duplicates nondet/Nondet_Reader_Option.thy but for the trace monad
instead. It proves various lemmas connecting reader_option concepts with
trace concepts.

Signed-off-by: Corey Lewis <[email protected]>
    @corlewis
    corlewis committed Mar 1, 2024
    Configuration menu
    Copy the full SHA
    a8e8f5e View commit details
    Browse the repository at this point in the history