diff options
| author | Christopher Pulte | 2016-10-25 12:08:27 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-10-25 12:08:27 +0100 |
| commit | b8fa3ef036d9a7e4ae2c3fe1274ac08f5aeb40b6 (patch) | |
| tree | 7003cc92c60c65f299e6ff71a6e85d540b45d0d3 /src/lem_interp | |
| parent | 92e4d2cd1221a55a1217e6c6a5dde9852fce7bce (diff) | |
shallow embedding fixes
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index cb4c0414..13a2dd38 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -1400,18 +1400,3 @@ instance (Eq decode_error) let (<>) = decode_error_inequal end - -val outcome_s_descrEqual : forall 's 'a. Eq 'a => outcome_s 's 'a -> outcome_s 's 'a -> bool -let outcome_s_descrEqual os1 os2 = match (fst os1,fst os2) with - | (Read_mem descr1 _, Read_mem descr2 _) -> descr1 = descr2 - | (Write_ea descr1 _, Write_ea descr2 _) -> descr1 = descr2 - | (Barrier descr1 _, Barrier descr2 _) -> descr1 = descr2 - | (Read_reg descr1 _, Read_reg descr2 _) -> descr1 = descr2 - | (Write_reg descr1 _, Write_reg descr2 _) -> descr1 = descr2 - | (Escape descr1 _, Escape descr2 _) -> descr1 = descr2 - | (Fail descr1, Fail descr2) -> descr1 = descr2 - | (Internal descr1 _, Internal descr2 _) -> descr1 = descr2 - | (Done a1, Done a2) -> a1 = a2 - | (Error e1, Error e2) -> e1 = e2 - | (Footprint _, Footprint _) -> true -end |