diff options
| author | Robert Norton | 2017-07-06 12:39:41 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-07-06 12:39:41 +0100 |
| commit | 06a1516244532f6c3c7223bf0dc407aac36ae3b1 (patch) | |
| tree | e427f393736d234a6bdd5e3a3a66fa15136e7102 | |
| parent | adaabb05518f68c5a2aea672920f7355b39b18cc (diff) | |
fix off by one in type of add_vec builtin function. There are many more dubious types but will wait for library rationalisation to fix.
| -rw-r--r-- | src/type_internal.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index 30e86f8a..155e78f4 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2082,7 +2082,7 @@ let initial_typ_env_list : (string * ((string * tannot) list)) list = lib_tannot ((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_range (mk_nv "q") (mk_2n (mk_nv "n"))))) + (mk_range (mk_nv "q") (mk_sub (mk_2n (mk_nv "n")) n_one)))) (Some "add_vec_vec_range") []; lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"); |