diff --git a/src/lib/state.ml b/src/lib/state.ml index 28b19d37e..f9bbcc3f5 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -843,6 +843,7 @@ let register_refs_lean doc_id doc_typ registers = [ string " set_"; idd; + space; colon; space; typp; @@ -850,11 +851,11 @@ let register_refs_lean doc_id doc_typ registers = 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 b/test/lean/registers.expected.lean similarity index 73% rename from test/lean/reg.expected.lean rename to test/lean/registers.expected.lean index 00e105040..88f30150e 100644 --- a/test/lean/reg.expected.lean +++ b/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 b/test/lean/registers.sail similarity index 100% rename from test/lean/reg.sail rename to test/lean/registers.sail