diff options
| author | Prashanth Mundkur | 2019-04-17 15:47:04 -0700 |
|---|---|---|
| committer | Prashanth Mundkur | 2019-04-17 15:47:04 -0700 |
| commit | ab040ce2e37489ed7446e10d7b5bcb26487b47e1 (patch) | |
| tree | d83837ef5d9885aa8cccdf65ec57f49bf3e1a547 /lib | |
| parent | 9e0f58f27966bf606bdc3ec06972bc294fbd362b (diff) | |
Add interpreter annots to vector_dec.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/vector_dec.sail | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index b4014aa6..ee84087e 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -143,11 +143,23 @@ val sub_bits = { val not_vec = {c: "not_bits", _: "not_vec"} : forall 'n. bits('n) -> bits('n) -val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val and_vec = { + lem: "and_vec", + c: "and_bits", + coq: "and_vec", + ocaml: "and_vec", + interpreter: "and_vec" +} : forall 'n. (bits('n), bits('n)) -> bits('n) overload operator & = {and_vec} -val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val or_vec = { + lem: "or_vec", + c: "or_bits", + coq: "or_vec", + ocaml: "or_vec", + interpreter: "or_vec" +} : forall 'n. (bits('n), bits('n)) -> bits('n) overload operator | = {or_vec} |
