diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index 0d4adab22..e014ff021 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/src/sail_lean_backend/pretty_print_lean.ml
@@ -867,10 +867,9 @@ let rec doc_defs_rec ctx defs types docdefs =
   | 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
+        if Env.is_extern (id_of_fundef fdef) env "lean" then docdefs
         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
diff --git a/test/lean/SailTinyArm.expected.lean b/test/lean/SailTinyArm.expected.lean
index b628d95f5..a40ad3473 100644
--- a/test/lean/SailTinyArm.expected.lean
+++ b/test/lean/SailTinyArm.expected.lean
@@ -512,6 +512,10 @@ instance : Arch where
 
 namespace Functions
 
+/-- Type quantifiers: k_ex6347# : Bool, k_ex6346# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
index b80e7dbef..316be290f 100644
--- a/test/lean/bitfield.expected.lean
+++ b/test/lean/bitfield.expected.lean
@@ -34,6 +34,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex700# : Bool, k_ex699# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
index 2c153d99b..036014c20 100644
--- a/test/lean/bitvec_operation.expected.lean
+++ b/test/lean/bitvec_operation.expected.lean
@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex779# : Bool, k_ex778# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
index dd04afea3..56b55f12f 100644
--- a/test/lean/enum.expected.lean
+++ b/test/lean/enum.expected.lean
@@ -26,6 +26,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex717# : Bool, k_ex716# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/errors.expected.lean b/test/lean/errors.expected.lean
index 260fe0db8..06c20eaaf 100644
--- a/test/lean/errors.expected.lean
+++ b/test/lean/errors.expected.lean
@@ -32,6 +32,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex731# : Bool, k_ex730# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
index 457a5bd40..95810439e 100644
--- a/test/lean/extern.expected.lean
+++ b/test/lean/extern.expected.lean
@@ -21,6 +21,75 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex1162# : Bool, k_ex1161# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
+/-- 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 spc_forwards (_ : Unit) : String :=
   " "
 
diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
index 1c3e9edb1..da5e1c972 100644
--- a/test/lean/extern_bitvec.expected.lean
+++ b/test/lean/extern_bitvec.expected.lean
@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex699# : Bool, k_ex698# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean
index d1f1ca83b..6203a618c 100644
--- a/test/lean/implicit.expected.lean
+++ b/test/lean/implicit.expected.lean
@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex789# : Bool, k_ex788# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/ite.expected.lean b/test/lean/ite.expected.lean
index 14125e2f1..0b10fc8db 100644
--- a/test/lean/ite.expected.lean
+++ b/test/lean/ite.expected.lean
@@ -36,6 +36,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex805# : Bool, k_ex804# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
index c28f9ecee..74b8a26fc 100644
--- a/test/lean/let.expected.lean
+++ b/test/lean/let.expected.lean
@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex772# : Bool, k_ex771# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/loop.expected.lean b/test/lean/loop.expected.lean
index c222f6a04..aed76b89d 100644
--- a/test/lean/loop.expected.lean
+++ b/test/lean/loop.expected.lean
@@ -32,6 +32,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex1303# : Bool, k_ex1302# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/mapping.expected.lean b/test/lean/mapping.expected.lean
index 5679c8e1c..3ca75eaf1 100644
--- a/test/lean/mapping.expected.lean
+++ b/test/lean/mapping.expected.lean
@@ -26,6 +26,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex852# : Bool, k_ex851# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
index 09177c670..8b8ab51cb 100644
--- a/test/lean/match.expected.lean
+++ b/test/lean/match.expected.lean
@@ -41,6 +41,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex797# : Bool, k_ex796# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/match_bv.expected.lean b/test/lean/match_bv.expected.lean
index 7796cbe93..893e3c36e 100644
--- a/test/lean/match_bv.expected.lean
+++ b/test/lean/match_bv.expected.lean
@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex1669# : Bool, k_ex1668# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/option.expected.lean b/test/lean/option.expected.lean
index cfa96302f..10bd58781 100644
--- a/test/lean/option.expected.lean
+++ b/test/lean/option.expected.lean
@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex699# : Bool, k_ex698# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean
index 822ddd0d2..e524a9654 100644
--- a/test/lean/range.expected.lean
+++ b/test/lean/range.expected.lean
@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex759# : Bool, k_ex758# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean
index 4e3409de0..9d92bdc54 100644
--- a/test/lean/register_vector.expected.lean
+++ b/test/lean/register_vector.expected.lean
@@ -96,6 +96,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex2434# : Bool, k_ex2433# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean
index 64c9561f4..89201af09 100644
--- a/test/lean/registers.expected.lean
+++ b/test/lean/registers.expected.lean
@@ -50,6 +50,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex873# : Bool, k_ex872# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
index e69c8cd8f..241734f9b 100644
--- a/test/lean/struct.expected.lean
+++ b/test/lean/struct.expected.lean
@@ -38,6 +38,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex760# : Bool, k_ex759# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/struct_of_enum.expected.lean b/test/lean/struct_of_enum.expected.lean
index 8c51994c6..b1ee0d8f3 100644
--- a/test/lean/struct_of_enum.expected.lean
+++ b/test/lean/struct_of_enum.expected.lean
@@ -30,6 +30,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex705# : Bool, k_ex704# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
index 7c94a34f6..32343527a 100644
--- a/test/lean/typedef.expected.lean
+++ b/test/lean/typedef.expected.lean
@@ -29,6 +29,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex715# : Bool, k_ex714# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x
diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
index c145c7b6e..ad2ab23ed 100644
--- a/test/lean/typquant.expected.lean
+++ b/test/lean/typquant.expected.lean
@@ -27,6 +27,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex737# : Bool, k_ex736# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x