diff options
| author | Brian Campbell | 2018-02-21 17:21:36 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-02-21 17:24:19 +0000 |
| commit | b044735b61daa98004b73bec930b24f5ed574c27 (patch) | |
| tree | 5592995c7ea916e57a04c6cf152b58ca96c0da74 /aarch64 | |
| parent | f3eef8c8587039570d08ce6dfb8a6163adfb3490 (diff) | |
Add more bitvector sizes for aarch64
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/mono/aarch64_extras.lem | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem index 4a32ad44..8af9ee5d 100644 --- a/aarch64/mono/aarch64_extras.lem +++ b/aarch64/mono/aarch64_extras.lem @@ -5,6 +5,12 @@ open import Sail_operators_mwords open import Prompt_monad open import State +type ty512 +instance (Size ty512) let size = 512 end +declare isabelle target_rep type ty512 = `512` +type ty1024 +instance (Size ty1024) let size = 1024 end +declare isabelle target_rep type ty1024 = `1024` type ty2048 instance (Size ty2048) let size = 2048 end declare isabelle target_rep type ty2048 = `2048` |