diff options
| author | Brian Campbell | 2019-09-16 13:27:02 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-09-19 17:03:06 +0100 |
| commit | 79f3f95d6b9b589867560ee9be267df5866afadd (patch) | |
| tree | 38e09c8aed3dd36d7b658fd1467ff85c6042ffb8 /lib/coq/Sail2_values.v | |
| parent | 4e1724e9c8856e38fd9683c018a43a434bf53565 (diff) | |
Expand Coq Hoare logic and congruence rules to more operators
Also tweak the informative and/or boolean definitions so that they use
the same proofs in both monads.
Diffstat (limited to 'lib/coq/Sail2_values.v')
0 files changed, 0 insertions, 0 deletions