diff options
| author | Thomas Bauereiss | 2017-10-13 16:22:11 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-10-13 17:23:39 +0100 |
| commit | c97dd66c7318a0a8c79bf5674a13fb7d799e3166 (patch) | |
| tree | 85b2e2424ef0ea439846e02b95bb2bb967e6fbc5 /lib | |
| parent | ecdbf28f72860cdb44ce9dc0bdd811b64572fd90 (diff) | |
Name (bit)vector operations more explicitly
Moreover, add support for pretty-printing (to Lem) vector access/update
operations for vectors with non-constant, but normalized start index.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/prelude.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index 215f63b2..e5b5004f 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -310,7 +310,7 @@ val extern forall Num 'n. [:'n:] -> [:2** 'n:] effect pure pow2 val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vector_length = "length" val extern forall Type 'a. list<'a> -> nat effect pure list_length -val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bvlength" +val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bitvector_length" overload length [bitvector_length; vector_length; list_length] |