summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
-rw-r--r--src/lem_interp/interp_inter_imp.lem2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index cf952953..4aacad5f 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -81,6 +81,8 @@ let rec extern_value mode for_mem optional_start v = match v with
if for_mem
then (Bytevector (to_bytes (from_bits bits)), Nothing)
else (Bitvector (from_bits bits) inc fst, Nothing)
+ | Interp.V_vector_sparse fst stop inc bits default ->
+ extern_value mode for_mem optional_start (Interp_lib.fill_in_sparse v)
| Interp.V_lit (L_aux L_zero _) ->
if for_mem
then (Bytevector [0],Nothing)