From 5342a052c43290b49dad1e2e1b8619581e3eceb5 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Fri, 14 Feb 2025 13:33:43 +0100
Subject: [PATCH] add more annotation, fix omitted fundefs (#1002)

---
 lib/generic_equality.sail                  |   7 +-
 lib/mapping.sail                           |   2 +-
 lib/string.sail                            |  20 +-
 lib/vector.sail                            |  12 +-
 src/sail_lean_backend/Sail/Sail.lean       |  14 ++
 src/sail_lean_backend/pretty_print_lean.ml |  18 +-
 test/c/hello_world.expected.lean           |  75 +++++++
 test/lean/SailTinyArm.expected.lean        | 206 ++++++++++++++++++++
 test/lean/bitfield.expected.lean           |  75 +++++++
 test/lean/bitvec_operation.expected.lean   |  75 +++++++
 test/lean/enum.expected.lean               |  75 +++++++
 test/lean/errors.expected.lean             |  75 +++++++
 test/lean/extern.expected.lean             |  74 +++++++
 test/lean/extern.sail                      |  13 ++
 test/lean/extern_bitvec.expected.lean      |  75 +++++++
 test/lean/implicit.expected.lean           |  75 +++++++
 test/lean/ite.expected.lean                |  75 +++++++
 test/lean/let.expected.lean                |  75 +++++++
 test/lean/loop.expected.lean               |  75 +++++++
 test/lean/mapping.expected.lean            | 216 +++++++++++++++++++++
 test/lean/mapping.sail                     |  30 +++
 test/lean/match.expected.lean              |  75 +++++++
 test/lean/match_bv.expected.lean           |  75 +++++++
 test/lean/option.expected.lean             |  75 +++++++
 test/lean/range.expected.lean              |  75 +++++++
 test/lean/register_vector.expected.lean    |  75 +++++++
 test/lean/registers.expected.lean          |  75 +++++++
 test/lean/struct.expected.lean             |  75 +++++++
 test/lean/struct_of_enum.expected.lean     |  75 +++++++
 test/lean/typedef.expected.lean            |  75 +++++++
 test/lean/typquant.expected.lean           |  75 +++++++
 31 files changed, 2097 insertions(+), 15 deletions(-)
 create mode 100644 test/lean/mapping.expected.lean
 create mode 100644 test/lean/mapping.sail

diff --git a/lib/generic_equality.sail b/lib/generic_equality.sail
index 155439997..0142c196c 100644
--- a/lib/generic_equality.sail
+++ b/lib/generic_equality.sail
@@ -53,9 +53,12 @@ val eq_anything = pure {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic
 
 overload operator == = {eq_anything}
 
-val neq_anything = pure {lem: "neq", lean: "Ne", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
+val neq_anything = pure {
+  lem: "neq",
+  lean: "Ne",
+  coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
 
-function neq_anything(x, y) = not_bool(eq_anything(x, y))
+function neq_anything(x, y) = not_bool(eq_anything(y, x))
 
 overload operator != = {neq_anything}
 
diff --git a/lib/mapping.sail b/lib/mapping.sail
index dfb314e6c..da0fa80d4 100644
--- a/lib/mapping.sail
+++ b/lib/mapping.sail
@@ -80,7 +80,7 @@ val string_startswith = pure {
   _: "string_startswith"
 }: (string, string) -> bool
 
-val n_leading_spaces = pure { coq: "n_leading_spaces_Z" } : string -> nat
+val n_leading_spaces = pure { coq: "n_leading_spaces_Z", lean: "String.leadingSpaces" } : string -> nat
 function n_leading_spaces s =
   match s {
     "" => 0,
diff --git a/lib/string.sail b/lib/string.sail
index d2c491ab4..d43f234cf 100644
--- a/lib/string.sail
+++ b/lib/string.sail
@@ -49,19 +49,31 @@ $define _STRING
 
 $include <arith.sail>
 
-val eq_string = pure {lem: "eq", coq: "generic_eq", _: "eq_string"} : (string, string) -> bool
+val eq_string = pure {
+   lem: "eq",
+   coq: "generic_eq",
+   lean: "Eq",
+   _: "eq_string"} : (string, string) -> bool
 
 overload operator == = {eq_string}
 
-val concat_str = pure {coq: "String.append", lem: "stringAppend", _: "concat_str"} : (string, string) -> string
+val concat_str = pure {
+   coq: "String.append",
+   lem: "stringAppend",
+   lean: "HAppend.hAppend",
+   _: "concat_str"} : (string, string) -> string
 
-val dec_str = pure "dec_str" : int -> string
+val dec_str = pure {
+  lean: "Int.repr",
+  _: "dec_str"} : int -> string
 
 val hex_str = pure "hex_str" : int -> string
 
 val hex_str_upper = pure "hex_str_upper" : int -> string
 
-val bits_str = pure "string_of_bits" : forall 'n. bitvector('n, dec) -> string
+val bits_str = pure {
+   lean: "BitVec.toHex",
+   _: "string_of_bits"} : forall 'n. bitvector('n, dec) -> string
 
 val concat_str_bits : forall 'n. (string, bitvector('n, dec)) -> string
 
diff --git a/lib/vector.sail b/lib/vector.sail
index 1b3aeecdd..4bb97c2d5 100644
--- a/lib/vector.sail
+++ b/lib/vector.sail
@@ -342,16 +342,22 @@ $endif
 
 overload vector_update_subrange = {update_subrange_bits}
 
-val sail_shiftleft = pure "shiftl" : forall 'n ('ord : Order).
+val sail_shiftleft = pure {
+  lean: "HShiftLeft.hShiftLeft",
+  _: "shiftl"} : forall 'n ('ord : Order).
     (bitvector('n, 'ord), int) -> bitvector('n, 'ord)
 
-val sail_shiftright = pure "shiftr" : forall 'n ('ord : Order).
+val sail_shiftright = pure {
+  lean: "HShiftRight.hShiftRight",
+  _: "shiftr"} : forall 'n ('ord : Order).
     (bitvector('n, 'ord), int) -> bitvector('n, 'ord)
 
 val sail_arith_shiftright = pure "arith_shiftr" : forall 'n ('ord : Order).
     (bitvector('n, 'ord), int) -> bitvector('n, 'ord)
 
-val sail_zeros = pure "zeros" : forall 'n, 'n >= 0. int('n) -> bits('n)
+val sail_zeros = pure {
+  lean: "BitVec.zero",
+  _: "zeros" }: forall 'n, 'n >= 0. int('n) -> bits('n)
 
 val sail_ones : forall 'n, 'n >= 0. int('n) -> bits('n)
 
diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean
index 610405003..e46b7569d 100644
--- a/src/sail_lean_backend/Sail/Sail.lean
+++ b/src/sail_lean_backend/Sail/Sail.lean
@@ -346,4 +346,18 @@ def shiftr (a : Int) (n : Int) : Int :=
   | Int.negSucc n => Sail.Nat.iterate (fun x => x * 2) (n+1) a
 
 end Int
+
+def String.leadingSpaces (s : String) : Nat :=
+  s.length - (s.dropWhile (· = ' ')).length
+
+
+instance : HShiftLeft (BitVec w) Int (BitVec w) where
+  hShiftLeft b i :=
+    match i with
+    | .ofNat n => BitVec.shiftLeft b n
+    | .negSucc n => BitVec.ushiftRight b n
+
+instance : HShiftRight (BitVec w) Int (BitVec w) where
+  hShiftRight b i := b <<< (-i)
+
 end Sail
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index 129229ffd..9495faf1e 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/src/sail_lean_backend/pretty_print_lean.ml
@@ -236,9 +236,11 @@ and doc_typ ctx (Typ_aux (t, _) as typ) =
       underscore (* TODO check if the type of implicit arguments can really be always inferred *)
   | Typ_app (Id_aux (Id "option", _), [A_aux (A_typ typ, _)]) -> parens (string "Option " ^^ doc_typ ctx typ)
   | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctx) ts)
-  | Typ_id (Id_aux (Id id, _)) -> string id
+  | Typ_id id -> doc_id_ctor id
   | Typ_app (Id_aux (Id "range", _), [A_aux (A_nexp low, _); A_aux (A_nexp high, _)]) ->
       if provably_nneg ctx low then string "Nat" else string "Int"
+  | Typ_app (Id_aux (Id "result", _), [A_aux (A_typ typ1, _); A_aux (A_typ typ2, _)]) ->
+      parens (separate space [string "Result"; doc_typ ctx typ1; doc_typ ctx typ2])
   | Typ_var kid -> doc_kid ctx kid
   | Typ_app (id, args) -> doc_id_ctor id ^^ space ^^ separate_map space (doc_typ_arg ctx `Only_relevant) args
   | Typ_exist (_, _, typ) -> doc_typ ctx typ
@@ -712,7 +714,7 @@ let doc_funcl ctx funcl =
   let comment, signature, ctx, fixup_binders = doc_funcl_init ctx.global funcl in
   comment ^^ nest 2 (signature ^^ hardline ^^ doc_funcl_body fixup_binders ctx funcl)
 
-let doc_fundef ctx (FD_aux (FD_function (r, typa, fcls), fannot)) =
+let doc_fundef ctx (FD_aux (FD_function (r, typa, fcls), fannot) as full_fundef) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
   | [funcl] -> doc_funcl ctx funcl
@@ -797,8 +799,14 @@ let doc_val ctx pat exp =
 let rec doc_defs_rec ctx defs types docdefs =
   match defs with
   | [] -> (types, docdefs)
-  | DEF_aux (DEF_fundef fdef, _) :: defs' ->
-      doc_defs_rec ctx defs' types (docdefs ^^ group (doc_fundef ctx fdef) ^/^ hardline)
+  | DEF_aux (DEF_fundef fdef, dannot) :: defs' ->
+      let env = dannot.env in
+      let pp_f =
+        if Env.is_extern (id_of_fundef fdef) env "lean" then empty
+        else docdefs ^^ group (doc_fundef ctx fdef) ^/^ hardline
+      in
+
+      doc_defs_rec ctx defs' types pp_f
   | DEF_aux (DEF_type tdef, _) :: defs' when List.mem (string_of_id (id_of_type_def tdef)) !opt_extern_types ->
       doc_defs_rec ctx defs' types docdefs
   | DEF_aux (DEF_type tdef, _) :: defs' ->
@@ -898,7 +906,7 @@ let main_function_stub =
 
 let pp_ast_lean (env : Type_check.env) effect_info ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o =
   (* TODO: remove the following line once we can handle the includes *)
-  let defs = remove_imports defs 0 in
+  (* let defs = remove_imports defs 0 in *)
   let regs = State.find_registers defs in
   let global = { effect_info } in
   let ctx = context_init env global in
diff --git a/test/c/hello_world.expected.lean b/test/c/hello_world.expected.lean
index d717daa15..1faa595aa 100644
--- a/test/c/hello_world.expected.lean
+++ b/test/c/hello_world.expected.lean
@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def sail_main (_ : Unit) : SailM Unit := do
   (print_endline_effect "Hello, World!")
 
diff --git a/test/lean/SailTinyArm.expected.lean b/test/lean/SailTinyArm.expected.lean
index b1dbd3d47..fc1735bc6 100644
--- a/test/lean/SailTinyArm.expected.lean
+++ b/test/lean/SailTinyArm.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev MAIRType := (BitVec 64)
 
 abbrev S1PIRType := (BitVec 64)
@@ -496,6 +506,71 @@ instance : Arch where
   arch_ak := arm_acc_type
   sys_reg_id := Unit
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def undefined_MAIRType (_ : Unit) : SailM (BitVec 64) := do
   (undefined_bitvector 64)
 
@@ -1899,6 +1974,137 @@ def fetch_and_execute (_ : Unit) : SailM Unit := do
   | some instr => (execute instr)
   | none => assert false "Unsupported Encoding"
 
+/-- Type quantifiers: k_a : Type, k_b : Type -/
+def is_ok (r : (Result k_a k_b)) : Bool :=
+  match r with
+  | Ok _ => true
+  | Err _ => false
+
+/-- Type quantifiers: k_a : Type, k_b : Type -/
+def is_err (r : (Result k_a k_b)) : Bool :=
+  match r with
+  | Ok _ => false
+  | Err _ => true
+
+/-- Type quantifiers: k_a : Type, k_b : Type -/
+def ok_option (r : (Result k_a k_b)) : (Option k_a) :=
+  match r with
+  | Ok x => (some x)
+  | Err _ => none
+
+/-- Type quantifiers: k_a : Type, k_b : Type -/
+def err_option (r : (Result k_a k_b)) : (Option k_b) :=
+  match r with
+  | Ok _ => none
+  | Err err => (some err)
+
+/-- Type quantifiers: k_a : Type, k_b : Type -/
+def unwrap_or (r : (Result k_a k_b)) (y : k_a) : k_a :=
+  match r with
+  | Ok x => x
+  | Err _ => y
+
+/-- Type quantifiers: k_n : Nat, k_n > 0 -/
+def sail_instr_announce (x : (BitVec k_n)) : Unit :=
+  ()
+
+/-- Type quantifiers: x : Nat, x ∈ {32, 64} -/
+def sail_branch_announce (x : Nat) (x : (BitVec x)) : Unit :=
+  ()
+
+def sail_reset_registers (_ : Unit) : Unit :=
+  ()
+
+def sail_synchronize_registers (_ : Unit) : Unit :=
+  ()
+
+/-- Type quantifiers: k_a : Type -/
+def sail_mark_register (x : (RegisterRef RegisterType k_a)) (x : String) : Unit :=
+  ()
+
+/-- Type quantifiers: k_a : Type, k_b : Type -/
+def sail_mark_register_pair (x : (RegisterRef RegisterType k_a)) (x : (RegisterRef RegisterType k_b)) (x : String) : Unit :=
+  ()
+
+/-- Type quantifiers: k_a : Type -/
+def sail_ignore_write_to (reg : (RegisterRef RegisterType k_a)) : Unit :=
+  (sail_mark_register reg "ignore_write")
+
+/-- Type quantifiers: k_a : Type -/
+def sail_pick_dependency (reg : (RegisterRef RegisterType k_a)) : Unit :=
+  (sail_mark_register reg "pick")
+
+/-- Type quantifiers: k_n : Nat, k_n ≥ 0 -/
+def __monomorphize (bv : (BitVec k_n)) : (BitVec k_n) :=
+  bv
+
+def undefined_Access_variety (_ : Unit) : SailM Access_variety := do
+  (internal_pick [AV_plain, AV_exclusive, AV_atomic_rmw])
+
+/-- Type quantifiers: arg_ : Nat, 0 ≤ arg_ ∧ arg_ ≤ 2 -/
+def Access_variety_of_num (arg_ : Nat) : Access_variety :=
+  match arg_ with
+  | 0 => AV_plain
+  | 1 => AV_exclusive
+  | _ => AV_atomic_rmw
+
+def num_of_Access_variety (arg_ : Access_variety) : Int :=
+  match arg_ with
+  | AV_plain => 0
+  | AV_exclusive => 1
+  | AV_atomic_rmw => 2
+
+def undefined_Access_strength (_ : Unit) : SailM Access_strength := do
+  (internal_pick [AS_normal, AS_rel_or_acq, AS_acq_rcpc])
+
+/-- Type quantifiers: arg_ : Nat, 0 ≤ arg_ ∧ arg_ ≤ 2 -/
+def Access_strength_of_num (arg_ : Nat) : Access_strength :=
+  match arg_ with
+  | 0 => AS_normal
+  | 1 => AS_rel_or_acq
+  | _ => AS_acq_rcpc
+
+def num_of_Access_strength (arg_ : Access_strength) : Int :=
+  match arg_ with
+  | AS_normal => 0
+  | AS_rel_or_acq => 1
+  | AS_acq_rcpc => 2
+
+def undefined_Explicit_access_kind (_ : Unit) : SailM Explicit_access_kind := do
+  (pure { variety := (← (undefined_Access_variety ()))
+          strength := (← (undefined_Access_strength ())) })
+
+/-- Type quantifiers: k_n : Nat, k_vasize : Nat, k_pa : Type, k_translation_summary : Type, k_arch_ak
+  : Type, k_n > 0 ∧ k_vasize > 0 -/
+def mem_read_request_is_exclusive (request : Mem_read_request k_n k_vasize k_pa k_translation_summary k_arch_ak) : Bool :=
+  match request.access_kind with
+  | AK_explicit eak =>
+    match eak.variety with
+    | AV_exclusive => true
+    | _ => false
+  | _ => false
+
+/-- Type quantifiers: k_n : Nat, k_vasize : Nat, k_pa : Type, k_translation_summary : Type, k_arch_ak
+  : Type, k_n > 0 ∧ k_vasize > 0 -/
+def mem_read_request_is_ifetch (request : Mem_read_request k_n k_vasize k_pa k_translation_summary k_arch_ak) : Bool :=
+  match request.access_kind with
+  | AK_ifetch () => true
+  | _ => false
+
+def __monomorphize_reads : Bool := false
+
+def __monomorphize_writes : Bool := false
+
+/-- Type quantifiers: k_n : Nat, k_vasize : Nat, k_pa : Type, k_translation_summary : Type, k_arch_ak
+  : Type, k_n > 0 ∧ k_vasize > 0 -/
+def mem_write_request_is_exclusive (request : Mem_write_request k_n k_vasize k_pa k_translation_summary k_arch_ak) : Bool :=
+  match request.access_kind with
+  | AK_explicit eak =>
+    match eak.variety with
+    | AV_exclusive => true
+    | _ => false
+  | _ => false
+
 def pa_bits (bv : (BitVec 56)) : (BitVec 64) :=
   (Sail.BitVec.zeroExtend bv 64)
 
diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
index bbfef3860..2a92520e0 100644
--- a/test/lean/bitfield.expected.lean
+++ b/test/lean/bitfield.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev cr_type := (BitVec 8)
 
 inductive Register : Type where
@@ -18,6 +28,71 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 8)) where
   default := .Reg R
 abbrev SailM := PreSailM RegisterType trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def undefined_cr_type (_ : Unit) : SailM (BitVec 8) := do
   (undefined_bitvector 8)
 
diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
index f922b1ad1..101d37078 100644
--- a/test/lean/bitvec_operation.expected.lean
+++ b/test/lean/bitvec_operation.expected.lean
@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def bitvector_eq (x : (BitVec 16)) (y : (BitVec 16)) : Bool :=
   (Eq x y)
 
diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
index ed9ce41c3..59f501770 100644
--- a/test/lean/enum.expected.lean
+++ b/test/lean/enum.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 inductive E where | A | B | C
   deriving Inhabited, DecidableEq
 
@@ -10,6 +20,71 @@ open E
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def undefined_E (_ : Unit) : SailM E := do
   (internal_pick [A, B, C])
 
diff --git a/test/lean/errors.expected.lean b/test/lean/errors.expected.lean
index c0ecb9646..89fee64e1 100644
--- a/test/lean/errors.expected.lean
+++ b/test/lean/errors.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 inductive Register : Type where
   | dummy
   deriving DecidableEq, Hashable
@@ -16,6 +26,71 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 1)) where
   default := .Reg dummy
 abbrev SailM := PreSailM RegisterType trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 /-- Type quantifiers: k_ex824# : Bool -/
 def test_exit (b : Bool) : SailM Unit := do
   if b
diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
index 52149b49c..3431d0a27 100644
--- a/test/lean/extern.expected.lean
+++ b/test/lean/extern.expected.lean
@@ -3,8 +3,73 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+def spc_forwards (_ : Unit) : String :=
+  " "
+
+def spc_forwards_matches (_ : Unit) : Bool :=
+  true
+
+def spc_backwards (x : String) : Unit :=
+  ()
+
+def spc_backwards_matches (s : String) : Bool :=
+  let len := (String.length s)
+  (Bool.and (Eq (String.leadingSpaces s) len) (GT.gt len 0))
+
+def opt_spc_forwards (_ : Unit) : String :=
+  ""
+
+def opt_spc_forwards_matches (_ : Unit) : Bool :=
+  true
+
+def opt_spc_backwards (x : String) : Unit :=
+  ()
+
+def opt_spc_backwards_matches (s : String) : Bool :=
+  (Eq (String.leadingSpaces s) (String.length s))
+
+def def_spc_forwards (_ : Unit) : String :=
+  " "
+
+def def_spc_forwards_matches (_ : Unit) : Bool :=
+  true
+
+def def_spc_backwards (x : String) : Unit :=
+  ()
+
+def def_spc_backwards_matches (s : String) : Bool :=
+  (Eq (String.leadingSpaces s) (String.length s))
+
+def sep_forwards (arg_ : Unit) : String :=
+  match arg_ with
+  | () =>
+    (String.append (opt_spc_forwards ())
+      (String.append "," (String.append (def_spc_forwards ()) "")))
+
+def sep_backwards (arg_ : String) : SailM Unit := do
+  match arg_ with
+  | _ => throw Error.Exit
+
+def sep_forwards_matches (arg_ : Unit) : Bool :=
+  match arg_ with
+  | () => true
+
+def sep_backwards_matches (arg_ : String) : SailM Bool := do
+  match arg_ with
+  | _ => throw Error.Exit
+
 def extern_add (_ : Unit) : Int :=
   (HAdd.hAdd 5 4)
 
@@ -114,6 +179,15 @@ def extern_string_append (_ : Unit) : String :=
 def extern_string_startswith (_ : Unit) : Bool :=
   (String.startsWith "Hello, world" "Hello")
 
+def extern_eq_string (_ : Unit) : Bool :=
+  (Eq "Hello" "world")
+
+def extern_concat_str (_ : Unit) : String :=
+  (HAppend.hAppend "Hello, " "world")
+
+def extern_n_leading_spaces (_ : Unit) : Nat :=
+  (String.leadingSpaces "   Belated Hello world!")
+
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
diff --git a/test/lean/extern.sail b/test/lean/extern.sail
index 1fb5b188b..c98fafba6 100644
--- a/test/lean/extern.sail
+++ b/test/lean/extern.sail
@@ -156,3 +156,16 @@ function extern_string_append() -> string = {
 function extern_string_startswith() -> bool = {
   return string_startswith("Hello, world", "Hello")
 }
+
+function extern_eq_string() -> bool = {
+  return eq_string("Hello", "world")
+}
+
+function extern_concat_str() -> string = {
+  return concat_str("Hello, ", "world")
+}
+
+function extern_n_leading_spaces() -> nat = {
+  return n_leading_spaces("   Belated Hello world!")
+}
+
diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
index 382be1a2d..2bbaa378e 100644
--- a/test/lean/extern_bitvec.expected.lean
+++ b/test/lean/extern_bitvec.expected.lean
@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def extern_const (_ : Unit) : (BitVec 64) :=
   (0xFFFF000012340000 : (BitVec 64))
 
diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean
index 403d74e4b..eb13db8bb 100644
--- a/test/lean/implicit.expected.lean
+++ b/test/lean/implicit.expected.lean
@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 /-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/
 def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=
   (Sail.BitVec.zeroExtend v m)
diff --git a/test/lean/ite.expected.lean b/test/lean/ite.expected.lean
index a15cee9c7..022cfe2d2 100644
--- a/test/lean/ite.expected.lean
+++ b/test/lean/ite.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 inductive Register : Type where
   | B
   | R
@@ -20,6 +30,71 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
   default := .Reg R
 abbrev SailM := PreSailM RegisterType trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 /-- Type quantifiers: n : Nat, 0 ≤ n -/
 def elif (n : Nat) : (BitVec 1) :=
   if (Eq n 0)
diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
index 559e2ba14..8df0f37d8 100644
--- a/test/lean/let.expected.lean
+++ b/test/lean/let.expected.lean
@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def foo (_ : Unit) : (BitVec 16) :=
   let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))
   (HAnd.hAnd (0x0000 : (BitVec 16)) z)
diff --git a/test/lean/loop.expected.lean b/test/lean/loop.expected.lean
index a38b45138..0180c568c 100644
--- a/test/lean/loop.expected.lean
+++ b/test/lean/loop.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 inductive Register : Type where
   | r
   deriving DecidableEq, Hashable
@@ -16,6 +26,71 @@ instance : Inhabited (RegisterRef RegisterType Int) where
   default := .Reg r
 abbrev SailM := PreSailM RegisterType trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 /-- Type quantifiers: n : Nat, m : Nat, 0 ≤ m, 0 ≤ n -/
 def foreachloop (m : Nat) (n : Nat) : Int :=
   let res : Int := 0
diff --git a/test/lean/mapping.expected.lean b/test/lean/mapping.expected.lean
new file mode 100644
index 000000000..15e38884d
--- /dev/null
+++ b/test/lean/mapping.expected.lean
@@ -0,0 +1,216 @@
+import Out.Sail.Sail
+import Out.Sail.BitVec
+
+open Sail
+
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
+inductive word_width where | BYTE | HALF | WORD | DOUBLE
+  deriving Inhabited, DecidableEq
+
+open word_width
+
+abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
+
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
+def undefined_word_width (_ : Unit) : SailM word_width := do
+  (internal_pick [BYTE, HALF, WORD, DOUBLE])
+
+/-- Type quantifiers: arg_ : Nat, 0 ≤ arg_ ∧ arg_ ≤ 3 -/
+def word_width_of_num (arg_ : Nat) : word_width :=
+  match arg_ with
+  | 0 => BYTE
+  | 1 => HALF
+  | 2 => WORD
+  | _ => DOUBLE
+
+def num_of_word_width (arg_ : word_width) : Int :=
+  match arg_ with
+  | BYTE => 0
+  | HALF => 1
+  | WORD => 2
+  | DOUBLE => 3
+
+def size_bits_forwards (arg_ : word_width) : (BitVec 2) :=
+  match arg_ with
+  | BYTE => (0b00 : (BitVec 2))
+  | HALF => (0b01 : (BitVec 2))
+  | WORD => (0b10 : (BitVec 2))
+  | DOUBLE => (0b11 : (BitVec 2))
+
+def size_bits_backwards (arg_ : (BitVec 2)) : word_width :=
+  let b__0 := arg_
+  if (Eq b__0 (0b00 : (BitVec 2)))
+  then BYTE
+  else if (Eq b__0 (0b01 : (BitVec 2)))
+       then HALF
+       else if (Eq b__0 (0b10 : (BitVec 2)))
+            then WORD
+            else DOUBLE
+
+def size_bits_forwards_matches (arg_ : word_width) : Bool :=
+  match arg_ with
+  | BYTE => true
+  | HALF => true
+  | WORD => true
+  | DOUBLE => true
+
+def size_bits_backwards_matches (arg_ : (BitVec 2)) : Bool :=
+  let b__0 := arg_
+  if (Eq b__0 (0b00 : (BitVec 2)))
+  then true
+  else if (Eq b__0 (0b01 : (BitVec 2)))
+       then true
+       else if (Eq b__0 (0b10 : (BitVec 2)))
+            then true
+            else if (Eq b__0 (0b11 : (BitVec 2)))
+                 then true
+                 else false
+
+def size_bits2_forwards (arg_ : word_width) : (BitVec 2) :=
+  match arg_ with
+  | BYTE => (0b00 : (BitVec 2))
+  | HALF => (0b01 : (BitVec 2))
+  | WORD => (0b10 : (BitVec 2))
+  | DOUBLE => (0b11 : (BitVec 2))
+
+def size_bits2_backwards (arg_ : (BitVec 2)) : word_width :=
+  let b__0 := arg_
+  if (Eq b__0 (0b00 : (BitVec 2)))
+  then BYTE
+  else if (Eq b__0 (0b01 : (BitVec 2)))
+       then HALF
+       else if (Eq b__0 (0b10 : (BitVec 2)))
+            then WORD
+            else DOUBLE
+
+def size_bits2_forwards_matches (arg_ : word_width) : Bool :=
+  match arg_ with
+  | BYTE => true
+  | HALF => true
+  | WORD => true
+  | DOUBLE => true
+
+def size_bits2_backwards_matches (arg_ : (BitVec 2)) : Bool :=
+  let b__0 := arg_
+  if (Eq b__0 (0b00 : (BitVec 2)))
+  then true
+  else if (Eq b__0 (0b01 : (BitVec 2)))
+       then true
+       else if (Eq b__0 (0b10 : (BitVec 2)))
+            then true
+            else if (Eq b__0 (0b11 : (BitVec 2)))
+                 then true
+                 else false
+
+def size_bits3_forwards (arg_ : word_width) : (BitVec 2) :=
+  match arg_ with
+  | BYTE => (0b00 : (BitVec 2))
+  | HALF => (0b01 : (BitVec 2))
+  | WORD => (0b10 : (BitVec 2))
+  | DOUBLE => (0b11 : (BitVec 2))
+
+def size_bits3_backwards (arg_ : (BitVec 2)) : word_width :=
+  let b__0 := arg_
+  if (Eq b__0 (0b00 : (BitVec 2)))
+  then BYTE
+  else if (Eq b__0 (0b01 : (BitVec 2)))
+       then HALF
+       else if (Eq b__0 (0b10 : (BitVec 2)))
+            then WORD
+            else DOUBLE
+
+def size_bits3_forwards_matches (arg_ : word_width) : Bool :=
+  match arg_ with
+  | BYTE => true
+  | HALF => true
+  | WORD => true
+  | DOUBLE => true
+
+def size_bits3_backwards_matches (arg_ : (BitVec 2)) : Bool :=
+  let b__0 := arg_
+  if (Eq b__0 (0b00 : (BitVec 2)))
+  then true
+  else if (Eq b__0 (0b01 : (BitVec 2)))
+       then true
+       else if (Eq b__0 (0b10 : (BitVec 2)))
+            then true
+            else if (Eq b__0 (0b11 : (BitVec 2)))
+                 then true
+                 else false
+
+def initialize_registers (_ : Unit) : Unit :=
+  ()
+
diff --git a/test/lean/mapping.sail b/test/lean/mapping.sail
new file mode 100644
index 000000000..c11f3fc78
--- /dev/null
+++ b/test/lean/mapping.sail
@@ -0,0 +1,30 @@
+default Order dec
+
+$include <prelude.sail>
+
+enum word_width = BYTE | HALF | WORD | DOUBLE
+
+val size_bits : word_width <-> bits(2)
+
+mapping size_bits = {
+  BYTE   <-> 0b00,
+  HALF   <-> 0b01,
+  WORD   <-> 0b10,
+  DOUBLE <-> 0b11
+}
+
+mapping size_bits2 : word_width <-> bits(2) = {
+  BYTE   <-> 0b00,
+  HALF   <-> 0b01,
+  WORD   <-> 0b10,
+  DOUBLE <-> 0b11
+}
+
+mapping size_bits3 : word_width <-> bits(2) = {
+  BYTE <-> 0b00,
+  HALF <-> 0b01,
+  WORD <-> 0b10,
+  forwards  DOUBLE => 0b11, // forwards is left-to-right
+  backwards 0b11 => DOUBLE, // backwards is right-to-left
+}
+
diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
index 906b7cdff..d7732f6e0 100644
--- a/test/lean/match.expected.lean
+++ b/test/lean/match.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 inductive E where | A | B | C
   deriving Inhabited, DecidableEq
 
@@ -25,6 +35,71 @@ instance : Inhabited (RegisterRef RegisterType E) where
   default := .Reg r_A
 abbrev SailM := PreSailM RegisterType trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def undefined_E (_ : Unit) : SailM E := do
   (internal_pick [A, B, C])
 
diff --git a/test/lean/match_bv.expected.lean b/test/lean/match_bv.expected.lean
index f7cbce477..e6e74b5b9 100644
--- a/test/lean/match_bv.expected.lean
+++ b/test/lean/match_bv.expected.lean
@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def decode (v__0 : (BitVec 32)) : Bool :=
   if (Bool.and (Eq (Sail.BitVec.extractLsb v__0 31 24) (0xF8 : (BitVec 8)))
        (Bool.and (Eq (Sail.BitVec.extractLsb v__0 21 21) (0b1 : (BitVec 1)))
diff --git a/test/lean/option.expected.lean b/test/lean/option.expected.lean
index 13d190efc..c6fb19977 100644
--- a/test/lean/option.expected.lean
+++ b/test/lean/option.expected.lean
@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def match_option (x : (Option (BitVec 1))) : (BitVec 1) :=
   match x with
   | some x => x
diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean
index 6037aacdb..5a7ec9854 100644
--- a/test/lean/range.expected.lean
+++ b/test/lean/range.expected.lean
@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 /-- Type quantifiers: x : Nat, 0 ≤ x ∧ x ≤ 31 -/
 def f_int (x : Nat) : Int :=
   0
diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean
index e55d00dae..9cc5fb16d 100644
--- a/test/lean/register_vector.expected.lean
+++ b/test/lean/register_vector.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev reg_index := Nat
 
 inductive Register : Type where
@@ -80,6 +90,71 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 64)) where
   default := .Reg _PC
 abbrev SailM := PreSailM RegisterType trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def GPRs : (Vector (RegisterRef RegisterType (BitVec 64)) 31) :=
   #v[Reg R30, Reg R29, Reg R28, Reg R27, Reg R26, Reg R25, Reg R24, Reg R23, Reg R22, Reg R21,
     Reg R20, Reg R19, Reg R18, Reg R17, Reg R16, Reg R15, Reg R14, Reg R13, Reg R12, Reg R11,
diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean
index 1e2f3f53a..2779a10a5 100644
--- a/test/lean/registers.expected.lean
+++ b/test/lean/registers.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 inductive Register : Type where
   | BIT
   | NAT
@@ -34,6 +44,71 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
   default := .Reg NAT
 abbrev SailM := PreSailM RegisterType trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def test (_ : Unit) : SailM Int := do
   writeReg INT (HAdd.hAdd (← readReg INT) 1)
   readReg INT
diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
index 63ee58c35..203b12c94 100644
--- a/test/lean/struct.expected.lean
+++ b/test/lean/struct.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 
 structure My_struct where
   field1 : Int
@@ -22,6 +32,71 @@ structure Mem_write_request
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def undefined_My_struct (_ : Unit) : SailM My_struct := do
   (pure { field1 := (← (undefined_int ()))
           field2 := (← (undefined_bit ())) })
diff --git a/test/lean/struct_of_enum.expected.lean b/test/lean/struct_of_enum.expected.lean
index e2d402bba..ab55a0efc 100644
--- a/test/lean/struct_of_enum.expected.lean
+++ b/test/lean/struct_of_enum.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 inductive e_test where | VAL
   deriving Inhabited, DecidableEq
 
@@ -14,6 +24,71 @@ structure s_test where
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def undefined_e_test (_ : Unit) : SailM e_test := do
   (internal_pick [VAL])
 
diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
index 2fa9a4677..205fc556f 100644
--- a/test/lean/typedef.expected.lean
+++ b/test/lean/typedef.expected.lean
@@ -3,6 +3,16 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev xlen : Int := 64
 
 abbrev xlen_bytes : Int := 8
@@ -13,6 +23,71 @@ abbrev my_bits k_n := (BitVec k_n)
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 /-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/
 def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=
   (Sail.BitVec.zeroExtend v m)
diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
index 4f490d5a1..96c8ddaf3 100644
--- a/test/lean/typquant.expected.lean
+++ b/test/lean/typquant.expected.lean
@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 /-- Type quantifiers: n : Int -/
 def foo (n : Int) : (BitVec 4) :=
   (0xF : (BitVec 4))