summaryrefslogtreecommitdiff
path: root/aarch64/mono/aarch64_extras.lem
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/mono/aarch64_extras.lem')
-rw-r--r--aarch64/mono/aarch64_extras.lem6
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`