diff options
| author | Thomas Bauereiss | 2018-01-30 18:15:29 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-01-31 12:49:20 +0000 |
| commit | 3cad2ad60f5f5f05ef94ba38590539939d3ccda0 (patch) | |
| tree | aa58990cbecf5a0367990039321c0d7672dbddce /riscv | |
| parent | 0beb4619c72f2e1cc2123e278c1ed7744e350899 (diff) | |
Split base definitions of Lem monads and further built-ins (e.g. loop combinators)
Add Isabelle-specific theories imported directly after monad definitions, but
before other combinators. These theories contain lemmas that tell the function
package how to deal with monadic binds in function definitions.
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/riscv_extras_embed_sequential.lem | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras_embed_sequential.lem index 044b2aa3..2d28f3c2 100644 --- a/riscv/riscv_extras_embed_sequential.lem +++ b/riscv/riscv_extras_embed_sequential.lem @@ -4,6 +4,7 @@ open import Sail_impl_base open import Sail_values open import Sail_operators open import State +open import State_monad let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw |