Tweak to a cv_inline theorem

Co-authored-by: Magnus Myreen <myreen@chalmers.se>
CakeML · Mar 15, 2024 · 18509e7 · 18509e7
1 parent 9b018ee
commit 18509e7
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/cv_translator/cv_primScript.sml b/cv_translator/cv_primScript.sml
@@ -860,7 +860,8 @@ QED
 
 Theorem cv_inline_word_ror[cv_inline]:
   !r a. (a : 'a word) #>> r =
-    let d = dimindex (:'a);
+    let a = a;
+        d = dimindex (:'a);
         r = r MOD d
     in a << (d - r) || a >>> r
 Proof