Merge pull request #1677 from nikos-alexandris/mcandidate

myreen · web-flow · commit a406a513a977 · 2025-10-03T09:39:14.000+02:00
Fix `l3_equivalence_lemmas` for changes in theory syntax
diff --git a/examples/l3-machine-code/arm8/asl-equiv/l3_equivalence_lemmasScript.sml b/examples/l3-machine-code/arm8/asl-equiv/l3_equivalence_lemmasScript.sml
@@ -1,6 +1,6 @@
 Theory l3_equivalence_lemmas
 Ancestors
-  arm8_step arm8 armv86a_termination armv86a armv86a_types words
+  armv86a armv86a_termination armv86a_types arm8_step arm8 words
   bitstring list rich_list integer int_arith arithmetic
   l3_equivalence_misc
 Libs
@@ -842,6 +842,8 @@ Definition create_wmask_def[nocompute]:
   in wmask
 End
 
+val _ = monadsyntax.enable_monad "sail2_state_monad"
+
 Theorem DecodeBitMasks_64_lemma[local]:
   armv86a$DecodeBitMasks 64 immN imms immr immediate : (word64 # word64) M =
   do
