summaryrefslogtreecommitdiff
path: root/aarch64/mono/aarch64_extras.lem
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/mono/aarch64_extras.lem')
-rw-r--r--aarch64/mono/aarch64_extras.lem3
1 files changed, 3 insertions, 0 deletions
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index f9027593..fb1e4861 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -58,6 +58,9 @@ let hex_slice v len lo =
let bs = ext_list false (len + lo) bs in
return (of_bools (subrange_list false bs hi lo))
+val BigEndianReverse : forall 'rv 'n 'e. Size 'n => mword 'n -> monad 'rv (mword 'n) 'e
+let BigEndianReverse w = return (reverse_endianness w)
+
let internal_pick vs = return (head vs)
(* Use constants for undefined values for now *)