Fix lean style in state.ml

rems-project · Jan 20, 2025 · 290094b · 290094b
1 parent bdd48ad
commit 290094b
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/src/lib/state.ml b/src/lib/state.ml
@@ -843,18 +843,19 @@ let register_refs_lean doc_id doc_typ registers =
       [
         string "  set_";
         idd;
+        space;
         colon;
         space;
         typp;
         string " -> SailM Unit";
         hardline;
         string "  get_";
         idd;
+        space;
         colon;
         space;
-        string "SailM (";
+        string "SailM ";
         typp;
-        string ")";
       ]
   in
   let refs = separate_map hardline register_ref registers in

diff --git a/test/lean/reg.expected.lean → test/lean/registers.expected.lean b/test/lean/reg.expected.lean → test/lean/registers.expected.lean
@@ -3,8 +3,8 @@ import Out.Sail.Sail
 open Sail
 
 class MonadReg where
-  set_R0: (BitVec 64) -> SailM Unit
-  get_R0: SailM ((BitVec 64))
+  set_R0 : (BitVec 64) -> SailM Unit
+  get_R0 : SailM (BitVec 64)
 
 variable [MonadReg]
 

diff --git a/test/lean/reg.sail → test/lean/registers.sail b/test/lean/reg.sail → test/lean/registers.sail