diff options
| author | Thomas Bauereiss | 2019-08-14 15:18:37 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-08-14 18:02:03 +0100 |
| commit | e3c73232aafe15d06739e0552d517ad095b0bf70 (patch) | |
| tree | d49a639518c60ceb5ad25d03811cfa72304a1459 /src/gen_lib/sail2_prompt_monad.lem | |
| parent | e2e273eda09c707a78bd96b668db92381a6e524e (diff) | |
Inline reg_deref in Lem output
Diffstat (limited to 'src/gen_lib/sail2_prompt_monad.lem')
| -rw-r--r-- | src/gen_lib/sail2_prompt_monad.lem | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem index 28c0a27e..a35165b9 100644 --- a/src/gen_lib/sail2_prompt_monad.lem +++ b/src/gen_lib/sail2_prompt_monad.lem @@ -235,7 +235,7 @@ let read_reg_bitfield reg regfield = read_reg_aux (external_reg_field_whole reg regfield) >>= fun v -> return (extract_only_element v)*) -let reg_deref = read_reg +let inline reg_deref = read_reg val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ()) |