diff --git a/test/lean/atom_bool.expected.lean b/test/lean/atom_bool.expected.lean
index 54a41793d..cf23b1537 100644
--- a/test/lean/atom_bool.expected.lean
+++ b/test/lean/atom_bool.expected.lean
@@ -4,9 +4,9 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def foo : Bool :=
+def foo (lit : Unit) : Bool :=
   true
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
index 6cf260284..27600cdea 100644
--- a/test/lean/bitfield.expected.lean
+++ b/test/lean/bitfield.expected.lean
@@ -83,6 +83,6 @@ def _set_cr_type_LT (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 1
   let r := (← (reg_deref r_ref))
   writeRegRef r_ref (_update_cr_type_LT r v)
 
-def initialize_registers : SailM Unit := do
+def initialize_registers (lit : Unit) : SailM Unit := do
   writeReg R (← (undefined_cr_type ()))
 
diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
index 99562465f..e83f18f10 100644
--- a/test/lean/bitvec_operation.expected.lean
+++ b/test/lean/bitvec_operation.expected.lean
@@ -52,6 +52,6 @@ def bitvector_unsigned (x : (BitVec 16)) : Nat :=
 def bitvector_signed (x : (BitVec 16)) : Int :=
   (BitVec.toInt x)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
index 533b787bb..49e75ee38 100644
--- a/test/lean/enum.expected.lean
+++ b/test/lean/enum.expected.lean
@@ -8,7 +8,7 @@ open E
 
 abbrev SailM := StateM Unit
 
-def undefined_E : SailM E := do
+def undefined_E (lit : Unit) : SailM E := do
   sorry
 
 /-- Type quantifiers: arg_ : Int, 0 ≤ arg_ ∧ arg_ ≤ 2 -/
@@ -24,6 +24,6 @@ def num_of_E (arg_ : E) : Int :=
   | B => 1
   | C => 2
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
index 6b810e7b1..12f10bab8 100644
--- a/test/lean/extern.expected.lean
+++ b/test/lean/extern.expected.lean
@@ -4,42 +4,42 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def extern_add : Int :=
+def extern_add (lit : Unit) : Int :=
   (Int.add 5 4)
 
-def extern_sub : Int :=
+def extern_sub (lit : Unit) : Int :=
   (Int.sub 5 (-4))
 
-def extern_tdiv : Int :=
+def extern_tdiv (lit : Unit) : Int :=
   (Int.tdiv 5 4)
 
-def extern_tmod : Int :=
+def extern_tmod (lit : Unit) : Int :=
   (Int.tmod 5 4)
 
-def extern_tmod_positive : Int :=
+def extern_tmod_positive (lit : Unit) : Int :=
   (Int.tmod 5 4)
 
-def extern_negate : Int :=
+def extern_negate (lit : Unit) : Int :=
   (Int.neg (-5))
 
-def extern_mult : Int :=
+def extern_mult (lit : Unit) : Int :=
   (Int.mul 5 (-4))
 
-def extern_and : Bool :=
+def extern_and (lit : Unit) : Bool :=
   (Bool.and true false)
 
-def extern_and_no_flow : Bool :=
+def extern_and_no_flow (lit : Unit) : Bool :=
   (Bool.and true false)
 
-def extern_or : Bool :=
+def extern_or (lit : Unit) : Bool :=
   (Bool.or true false)
 
-def extern_eq_bool : Bool :=
+def extern_eq_bool (lit : Unit) : Bool :=
   (Eq true false)
 
-def extern_eq_bit : Bool :=
+def extern_eq_bit (lit : Unit) : Bool :=
   (Eq 0#1 1#1)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
index 9996aadae..d04ba2047 100644
--- a/test/lean/extern_bitvec.expected.lean
+++ b/test/lean/extern_bitvec.expected.lean
@@ -4,12 +4,12 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def extern_const : (BitVec 64) :=
+def extern_const (lit : Unit) : (BitVec 64) :=
   (0xFFFF000012340000 : (BitVec 64))
 
-def extern_add : (BitVec 16) :=
+def extern_add (lit : Unit) : (BitVec 16) :=
   (HAdd.hAdd (0xFFFF : (BitVec 16)) (0x1234 : (BitVec 16)))
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/ite.expected.lean b/test/lean/ite.expected.lean
index ba593375a..ad25b0858 100644
--- a/test/lean/ite.expected.lean
+++ b/test/lean/ite.expected.lean
@@ -42,7 +42,7 @@ def monadic_lines (n : Nat) : SailM Unit := do
        writeReg B b
   else writeReg B b
 
-def initialize_registers : SailM Unit := do
+def initialize_registers (lit : Unit) : SailM Unit := do
   writeReg R sorry
   writeReg B sorry
 
diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
index 0669173b7..7dbbb33a5 100644
--- a/test/lean/let.expected.lean
+++ b/test/lean/let.expected.lean
@@ -4,10 +4,10 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def foo : (BitVec 16) :=
+def foo (lit : Unit) : (BitVec 16) :=
   let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))
   (HAnd.hAnd (0x0000 : (BitVec 16)) z)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
index 5731a6361..205998d41 100644
--- a/test/lean/match.expected.lean
+++ b/test/lean/match.expected.lean
@@ -8,7 +8,7 @@ open E
 
 abbrev SailM := StateM Unit
 
-def undefined_E : SailM E := do
+def undefined_E (lit : Unit) : SailM E := do
   sorry
 
 def match_enum (x : E) : (BitVec 1) :=
@@ -33,6 +33,6 @@ def match_pair (arg0 : Int) (arg1 : Int) : Int :=
   match x with
   | (a, b) => (HAdd.hAdd a b)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean
index 0064ae423..75e97c156 100644
--- a/test/lean/range.expected.lean
+++ b/test/lean/range.expected.lean
@@ -24,6 +24,6 @@ def f_nnegvar (x : Nat) : Nat :=
 def f_unkn (x : Int) : Int :=
   x
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean
index a10520201..fe43f2b62 100644
--- a/test/lean/register_vector.expected.lean
+++ b/test/lean/register_vector.expected.lean
@@ -96,7 +96,7 @@ def rX (n : Nat) : SailM (BitVec 64) := do
   then (reg_deref (vectorAccess GPRs n))
   else (pure (0x0000000000000000 : (BitVec 64)))
 
-def rPC : SailM (BitVec 64) := do
+def rPC (lit : Unit) : SailM (BitVec 64) := do
   readReg _PC
 
 def wPC (pc : (BitVec 64)) : SailM Unit := do
@@ -110,7 +110,7 @@ def monad_test (r : Nat) : SailM (BitVec 1) := do
        then (pure 1#1)
        else (pure 0#1)
 
-def initialize_registers : SailM Unit := do
+def initialize_registers (lit : Unit) : SailM Unit := do
   writeReg _PC sorry
   writeReg R30 sorry
   writeReg R29 sorry
diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean
index f9eef1f0b..e34cb806a 100644
--- a/test/lean/registers.expected.lean
+++ b/test/lean/registers.expected.lean
@@ -33,11 +33,11 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
   default := .Reg NAT
 abbrev SailM := PreSailM RegisterType
 
-def test : SailM Int := do
+def test (lit : Unit) : SailM Int := do
   writeReg INT (HAdd.hAdd (← readReg INT) 1)
   readReg INT
 
-def initialize_registers : SailM Unit := do
+def initialize_registers (lit : Unit) : SailM Unit := do
   writeReg R0 sorry
   writeReg R1 sorry
   writeReg INT sorry
diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
index a049b15ca..81b7c0ca3 100644
--- a/test/lean/struct.expected.lean
+++ b/test/lean/struct.expected.lean
@@ -9,8 +9,8 @@ structure My_struct where
 abbrev SailM := StateM Unit
 
 def undefined_My_struct (lit : Unit) : SailM My_struct := do
-  (pure { field1 := (← sorry)
-          field2 := (← sorry) })
+  (pure { field1 := sorry
+          field2 := sorry })
 
 def struct_field2 (s : My_struct) : (BitVec 1) :=
   s.field2
@@ -30,6 +30,6 @@ def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
 def undef_struct (x : (BitVec 1)) : SailM My_struct := do
   ((undefined_My_struct ()) : SailM My_struct)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean
index 6cf56a2b1..36e800681 100644
--- a/test/lean/trivial.expected.lean
+++ b/test/lean/trivial.expected.lean
@@ -7,6 +7,6 @@ abbrev SailM := StateM Unit
 def foo (y : Unit) : Unit :=
   y
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean
index 65447e3cd..4811bf126 100644
--- a/test/lean/tuples.expected.lean
+++ b/test/lean/tuples.expected.lean
@@ -4,12 +4,12 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def tuple1 : (Int × Int × ((BitVec 2) × Unit)) :=
+def tuple1 (lit : Unit) : (Int × Int × ((BitVec 2) × Unit)) :=
   (3, 5, ((0b10 : (BitVec 2)), ()))
 
-def tuple2 : SailM (Int × Int) := do
+def tuple2 (lit : Unit) : SailM (Int × Int) := do
   (pure ((← sorry), (← sorry)))
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/type_kid.expected.lean b/test/lean/type_kid.expected.lean
index 2b4204a65..78d4c2c96 100644
--- a/test/lean/type_kid.expected.lean
+++ b/test/lean/type_kid.expected.lean
@@ -8,6 +8,6 @@ abbrev SailM := StateM Unit
 def foo (x : k_a) : (k_a × k_a) :=
   (x, x)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
index af8fe6222..c76f70ca8 100644
--- a/test/lean/typedef.expected.lean
+++ b/test/lean/typedef.expected.lean
@@ -18,6 +18,6 @@ def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=
 def EXTS {m : _} (v : (BitVec k_n)) : (BitVec m) :=
   (Sail.BitVec.signExtend v m)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
index 4e09ec3ec..5ea28afaa 100644
--- a/test/lean/typquant.expected.lean
+++ b/test/lean/typquant.expected.lean
@@ -12,6 +12,6 @@ def foo (n : Int) : (BitVec 4) :=
 def bar (x : (BitVec k_n)) : (BitVec k_n) :=
   x
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 
diff --git a/test/lean/union.expected.lean b/test/lean/union.expected.lean
index 2c020b766..292f1820c 100644
--- a/test/lean/union.expected.lean
+++ b/test/lean/union.expected.lean
@@ -24,11 +24,11 @@ open my_option
 abbrev SailM := StateM Unit
 
 def undefined_rectangle (lit : Unit) : SailM rectangle := do
-  (pure { width := (← sorry)
-          height := (← sorry) })
+  (pure { width := sorry
+          height := sorry })
 
 def undefined_circle (lit : Unit) : SailM circle := do
-  (pure { radius := (← sorry) })
+  (pure { radius := sorry })
 
 /-- Type quantifiers: k_a : Type -/
 def is_none (opt : my_option) : Bool :=
@@ -36,6 +36,6 @@ def is_none (opt : my_option) : Bool :=
   | MySome _ => false
   | MyNone () => true
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()