diff options
| author | Brian Campbell | 2018-05-10 14:52:31 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-05-10 14:52:31 +0100 |
| commit | 823fe1d82e753add2d54ba010689a81af027ba6d (patch) | |
| tree | abcd876e45736b3085d1f9f4e687aebe24ffe10b /lib/hol | |
| parent | 1f9418d9fe49dc671964fc826a2a8847e3255c9a (diff) | |
RISC-V in HOL4
Diffstat (limited to 'lib/hol')
| -rw-r--r-- | lib/hol/prompt_monad.lem | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/hol/prompt_monad.lem b/lib/hol/prompt_monad.lem index b1ef4bcc..4481f623 100644 --- a/lib/hol/prompt_monad.lem +++ b/lib/hol/prompt_monad.lem @@ -30,3 +30,6 @@ let inline write_tag = write_tagS let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz) let inline write_mem_val = write_mem_valS let barrier _ = return () + +let inline excl_result = excl_resultS +let inline assert_exp = assert_expS
\ No newline at end of file |