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.lem4
1 files changed, 1 insertions, 3 deletions
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index 1e91dd31..ffc8baf0 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -61,9 +61,7 @@ let hex_slice v len 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 *)
+(* Use constants for some undefined values for now *)
let undefined_string () = return ""
let undefined_unit () = return ()
let undefined_int () = return (0:ii)