diff options
| -rw-r--r-- | src/type_check.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 268183fe..58bd0d17 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -3272,6 +3272,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ()))) | E_vector_update (v, n, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update", [v; n; exp]), (l, ()))) | E_vector_update_subrange (v, n, m, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update_subrange", [v; n; m; exp]), (l, ()))) + | E_vector_append (v1, E_aux (E_vector [], _)) -> infer_exp env v1 | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "append", [v1; v2]), (l, ()))) | E_vector_subrange (v, n, m) -> infer_exp env (E_aux (E_app (mk_id "vector_subrange", [v; n; m]), (l, ()))) | E_vector [] -> typ_error l "Cannot infer type of empty vector" |