diff options
| author | Thomas Bauereiss | 2018-02-14 19:45:07 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-15 20:11:21 +0000 |
| commit | 737ec26cf494affb346504c482e9b91127b68636 (patch) | |
| tree | 30bcac2487eb2294952624aa25321a0299c6e2e7 /src/reporting_basic.ml | |
| parent | 9883998c6de1a0421eacb4f4c352b0aa8c4a1b5c (diff) | |
Rebase state monad onto prompt monad
Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad. Add some
Isabelle lemmas about the monad lifting.
Also drop the "_embed" and "_sequential" suffixes from names of generated
files.
Diffstat (limited to 'src/reporting_basic.ml')
0 files changed, 0 insertions, 0 deletions