diff options
| author | Christopher Pulte | 2016-10-06 17:23:28 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-10-06 17:23:28 +0100 |
| commit | 99fdb2e003b7433dc06372d2ffebd6d5111ce46d (patch) | |
| tree | f48c22ae3529fccd854877fa1b5490fea70d3ecb /src/gen_lib/vector.lem | |
| parent | 1d105202240057e8a1c5c835a2655cf8112167fe (diff) | |
move type definitions that both interpreter and shallow embedding use to sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome
Diffstat (limited to 'src/gen_lib/vector.lem')
| -rw-r--r-- | src/gen_lib/vector.lem | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem index b2d68132..6acb4aa0 100644 --- a/src/gen_lib/vector.lem +++ b/src/gen_lib/vector.lem @@ -1,6 +1,7 @@ open import Pervasives_extra -type bit = O | I | Undef +(* this is here to avoid circular dependencies when Sail_values imports Arch.lem *) +type bitU = O | I | Undef (* element list * start * has increasing direction *) type vector 'a = Vector of list 'a * integer * bool @@ -11,11 +12,6 @@ let rec nth xs (n : integer) = | _ -> failwith "nth applied to empty list" end -let to_bool = function - | O -> false - | I -> true - | Undef -> failwith "to_bool applied to Undef" - end let get_start (Vector _ s _) = s let length (Vector bs _ _) = integerFromNat (length bs) |
