diff options
| author | Brian Campbell | 2019-05-20 13:45:31 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-05-20 13:45:31 +0100 |
| commit | b87d1c27e4349cb85b9597a99c8024a59e2e0bac (patch) | |
| tree | 0cd70f24b0daee56780d801b2d3c9873f805e2fd /src/initial_check.ml | |
| parent | 97de43adb6f786c2af88ed6a4d14d330a9d59899 (diff) | |
Revert "Add constraints to undefined vector functions to ensure that lengths are"
This reverts commit 8bed4e4ef414f93e02f28f0e5eb223a855ba3d14.
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 3f5592ba..522faab7 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -923,9 +923,9 @@ let undefined_builtin_val_specs = extern_of_string (mk_id "undefined_string") "unit -> string effect {undef}"; extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}"; extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; - extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order), 'n >= 0. (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}"; - (* Only used with lem_mwords or coq *) - extern_of_string (mk_id "undefined_bitvector") "forall 'n, 'n >= 0. atom('n) -> vector('n, dec, bit) effect {undef}"; + extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}"; + (* Only used with lem_mwords *) + extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}"; extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"] let generate_undefineds vs_ids (Defs defs) = |