Rules and supporting files for building aarch64_small monomorphised Isabelle

1 files changed, 6 insertions, 0 deletions

diff --git a/aarch64_small/mono-splices/Replicate.sail b/aarch64_small/mono-splices/Replicate.sail
new file mode 100644
index 00000000..a3c464e5
--- /dev/null
+++ b/aarch64_small/mono-splices/Replicate.sail
@@ -0,0 +1,6 @@
+function Replicate(N, x) = {
+  assert(N % 'M == 0, "((N MOD M) == 0)");
+  let 'O = N / 'M;
+  assert(constraint('O * 'M == 'N));
+  return(replicate_bits(x, N / 'M))
+}