From d84040e000333d6d2a212fb849a38fb73a65eb48 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 Nov 2023 17:41:42 +0100
Subject: Regenerate the files

---
 tests/coq/traits/Traits.v        |  10 +--
 tests/fstar/traits/Traits.fst    |  10 +--
 tests/lean/Array.lean            |  26 +++---
 tests/lean/BetreeMain/Funs.lean  |  42 ++++-----
 tests/lean/External/Funs.lean    |   8 +-
 tests/lean/Hashmap/Funs.lean     |  40 ++++-----
 tests/lean/HashmapMain/Funs.lean |  38 ++++----
 tests/lean/Loops.lean            | 184 +++++++++++++++++++--------------------
 tests/lean/NoNestedBorrows.lean  | 133 ++++++++++++++--------------
 tests/lean/Paper.lean            |  32 +++----
 tests/lean/PoloniusList.lean     |   8 +-
 tests/lean/Traits.lean           |  10 +--
 12 files changed, 259 insertions(+), 282 deletions(-)

(limited to 'tests')

diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 0952a1df..50eaf848 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -382,15 +382,11 @@ Definition test_where2
   Return tt
 .
 
-(** [alloc::string::String]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 *)
-Axiom alloc_string_String_t : Type.
-
 (** Trait declaration: [traits::ParentTrait0]
     Source: 'src/traits.rs', lines 200:0-200:22 *)
 Record ParentTrait0_t (Self : Type) := mkParentTrait0_t {
   ParentTrait0_tParentTrait0_t_W : Type;
-  ParentTrait0_t_get_name : Self -> result alloc_string_String_t;
+  ParentTrait0_t_get_name : Self -> result string;
   ParentTrait0_t_get_w : Self -> result ParentTrait0_tParentTrait0_t_W;
 }.
 
@@ -419,9 +415,7 @@ Arguments ChildTrait_tChildTrait_t_ParentTrait1SelfInst { _ }.
 (** [traits::test_child_trait1]: forward function
     Source: 'src/traits.rs', lines 209:0-209:56 *)
 Definition test_child_trait1
-  (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) :
-  result alloc_string_String_t
-  :=
+  (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) : result string :=
   childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_name)
     x
 .
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 4cb9fbf1..895a1cac 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -307,15 +307,11 @@ let test_where2
   =
   Return ()
 
-(** [alloc::string::String]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 *)
-assume type alloc_string_String_t : Type0
-
 (** Trait declaration: [traits::ParentTrait0]
     Source: 'src/traits.rs', lines 200:0-200:22 *)
 noeq type parentTrait0_t (self : Type0) = {
   tW : Type0;
-  get_name : self -> result alloc_string_String_t;
+  get_name : self -> result string;
   get_w : self -> result tW;
 }
 
@@ -333,9 +329,7 @@ noeq type childTrait_t (self : Type0) = {
 (** [traits::test_child_trait1]: forward function
     Source: 'src/traits.rs', lines 209:0-209:56 *)
 let test_child_trait1
-  (t : Type0) (childTraitTInst : childTrait_t t) (x : t) :
-  result alloc_string_String_t
-  =
+  (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : result string =
   childTraitTInst.parentTrait0SelfInst.get_name x
 
 (** [traits::test_child_trait2]: forward function
diff --git a/tests/lean/Array.lean b/tests/lean/Array.lean
index 4832f469..b49add96 100644
--- a/tests/lean/Array.lean
+++ b/tests/lean/Array.lean
@@ -31,10 +31,10 @@ def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result (Slice T) :=
 /- [array::array_to_mut_slice_]: backward function 0
    Source: 'src/array.rs', lines 21:0-21:58 -/
 def array_to_mut_slice__back
-  (T : Type) (s : Array T 32#usize) (ret0 : Slice T) :
+  (T : Type) (s : Array T 32#usize) (ret : Slice T) :
   Result (Array T 32#usize)
   :=
-  Array.from_slice T 32#usize s ret0
+  Array.from_slice T 32#usize s ret
 
 /- [array::array_len]: forward function
    Source: 'src/array.rs', lines 25:0-25:40 -/
@@ -82,10 +82,10 @@ def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result T :=
 /- [array::index_mut_array]: backward function 0
    Source: 'src/array.rs', lines 52:0-52:62 -/
 def index_mut_array_back
-  (T : Type) (s : Array T 32#usize) (i : Usize) (ret0 : T) :
+  (T : Type) (s : Array T 32#usize) (i : Usize) (ret : T) :
   Result (Array T 32#usize)
   :=
-  Array.update_usize T 32#usize s i ret0
+  Array.update_usize T 32#usize s i ret
 
 /- [array::index_slice]: forward function
    Source: 'src/array.rs', lines 56:0-56:46 -/
@@ -100,8 +100,8 @@ def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result T :=
 /- [array::index_mut_slice]: backward function 0
    Source: 'src/array.rs', lines 60:0-60:58 -/
 def index_mut_slice_back
-  (T : Type) (s : Slice T) (i : Usize) (ret0 : T) : Result (Slice T) :=
-  Slice.update_usize T s i ret0
+  (T : Type) (s : Slice T) (i : Usize) (ret : T) : Result (Slice T) :=
+  Slice.update_usize T s i ret
 
 /- [array::slice_subslice_shared_]: forward function
    Source: 'src/array.rs', lines 64:0-64:70 -/
@@ -122,12 +122,12 @@ def slice_subslice_mut_
 /- [array::slice_subslice_mut_]: backward function 0
    Source: 'src/array.rs', lines 68:0-68:75 -/
 def slice_subslice_mut__back
-  (x : Slice U32) (y : Usize) (z : Usize) (ret0 : Slice U32) :
+  (x : Slice U32) (y : Usize) (z : Usize) (ret : Slice U32) :
   Result (Slice U32)
   :=
   core.slice.index.Slice.index_mut_back U32 (core.ops.range.Range Usize)
     (core.slice.index.SliceIndexRangeUsizeSliceTInst U32) x
-    { start := y, end_ := z } ret0
+    { start := y, end_ := z } ret
 
 /- [array::array_to_slice_shared_]: forward function
    Source: 'src/array.rs', lines 72:0-72:54 -/
@@ -142,8 +142,8 @@ def array_to_slice_mut_ (x : Array U32 32#usize) : Result (Slice U32) :=
 /- [array::array_to_slice_mut_]: backward function 0
    Source: 'src/array.rs', lines 76:0-76:59 -/
 def array_to_slice_mut__back
-  (x : Array U32 32#usize) (ret0 : Slice U32) : Result (Array U32 32#usize) :=
-  Array.from_slice U32 32#usize x ret0
+  (x : Array U32 32#usize) (ret : Slice U32) : Result (Array U32 32#usize) :=
+  Array.from_slice U32 32#usize x ret
 
 /- [array::array_subslice_shared_]: forward function
    Source: 'src/array.rs', lines 80:0-80:74 -/
@@ -166,13 +166,13 @@ def array_subslice_mut_
 /- [array::array_subslice_mut_]: backward function 0
    Source: 'src/array.rs', lines 84:0-84:79 -/
 def array_subslice_mut__back
-  (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret0 : Slice U32) :
+  (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret : Slice U32) :
   Result (Array U32 32#usize)
   :=
   core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 32#usize
     (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize)
     (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
-    { start := y, end_ := z } ret0
+    { start := y, end_ := z } ret
 
 /- [array::index_slice_0]: forward function
    Source: 'src/array.rs', lines 88:0-88:38 -/
@@ -417,7 +417,7 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
   let i := Slice.len U32 s
   let i0 := Slice.len U32 s2
   if not (i = i0)
-  then Result.fail Error.panic
+  then Result.fail .panic
   else sum2_loop s s2 0#u32 0#usize
 
 /- [array::f0]: forward function
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 45548884..4c862225 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -121,7 +121,7 @@ divergent def betree.List.split_at
         let (ls0, ls1) := p
         let l := ls0
         Result.ret (betree.List.Cons hd l, ls1)
-    | betree.List.Nil => Result.fail Error.panic
+    | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
    (there is a single backward function, and the forward function returns ())
@@ -138,7 +138,7 @@ def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret x
-  | betree.List.Nil => Result.fail Error.panic
+  | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
    Source: 'src/betree.rs', lines 306:4-306:32 -/
@@ -147,14 +147,14 @@ def betree.List.pop_front_back
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret tl
-  | betree.List.Nil => Result.fail Error.panic
+  | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
    Source: 'src/betree.rs', lines 318:4-318:22 -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
   | betree.List.Cons hd l => Result.ret hd
-  | betree.List.Nil => Result.fail Error.panic
+  | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
    Source: 'src/betree.rs', lines 327:4-327:44 -/
@@ -241,20 +241,20 @@ divergent def betree.Node.lookup_first_message_for_key
    Source: 'src/betree.rs', lines 789:4-792:34 -/
 divergent def betree.Node.lookup_first_message_for_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
-  (ret0 : betree.List (U64 × betree.Message)) :
+  (ret : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
   :=
   match msgs with
   | betree.List.Cons x next_msgs =>
     let (i, m) := x
     if i >= key
-    then Result.ret ret0
+    then Result.ret ret
     else
       do
         let next_msgs0 ←
-          betree.Node.lookup_first_message_for_key_back key next_msgs ret0
+          betree.Node.lookup_first_message_for_key_back key next_msgs ret
         Result.ret (betree.List.Cons (i, m) next_msgs0)
-  | betree.List.Nil => Result.ret ret0
+  | betree.List.Nil => Result.ret ret
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
    Source: 'src/betree.rs', lines 819:4-819:90 -/
@@ -271,8 +271,8 @@ divergent def betree.Node.apply_upserts
         let msg ← betree.List.pop_front (U64 × betree.Message) msgs
         let (_, m) := msg
         match m with
-        | betree.Message.Insert i => Result.fail Error.panic
-        | betree.Message.Delete => Result.fail Error.panic
+        | betree.Message.Insert i => Result.fail .panic
+        | betree.Message.Delete => Result.fail .panic
         | betree.Message.Upsert s =>
           do
             let v ← betree.upsert_update prev s
@@ -302,8 +302,8 @@ divergent def betree.Node.apply_upserts_back
         let msg ← betree.List.pop_front (U64 × betree.Message) msgs
         let (_, m) := msg
         match m with
-        | betree.Message.Insert i => Result.fail Error.panic
-        | betree.Message.Delete => Result.fail Error.panic
+        | betree.Message.Insert i => Result.fail .panic
+        | betree.Message.Delete => Result.fail .panic
         | betree.Message.Upsert s =>
           do
             let v ← betree.upsert_update prev s
@@ -542,7 +542,7 @@ divergent def betree.Node.lookup_first_message_after_key
    Source: 'src/betree.rs', lines 689:4-692:34 -/
 divergent def betree.Node.lookup_first_message_after_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
-  (ret0 : betree.List (U64 × betree.Message)) :
+  (ret : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
   :=
   match msgs with
@@ -552,10 +552,10 @@ divergent def betree.Node.lookup_first_message_after_key_back
     then
       do
         let next_msgs0 ←
-          betree.Node.lookup_first_message_after_key_back key next_msgs ret0
+          betree.Node.lookup_first_message_after_key_back key next_msgs ret
         Result.ret (betree.List.Cons (k, m) next_msgs0)
-    else Result.ret ret0
-  | betree.List.Nil => Result.ret ret0
+    else Result.ret ret
+  | betree.List.Nil => Result.ret ret
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
    (there is a single backward function, and the forward function returns ())
@@ -658,19 +658,19 @@ divergent def betree.Node.lookup_mut_in_bindings
    Source: 'src/betree.rs', lines 653:4-656:32 -/
 divergent def betree.Node.lookup_mut_in_bindings_back
   (key : U64) (bindings : betree.List (U64 × U64))
-  (ret0 : betree.List (U64 × U64)) :
+  (ret : betree.List (U64 × U64)) :
   Result (betree.List (U64 × U64))
   :=
   match bindings with
   | betree.List.Cons hd tl =>
     let (i, i0) := hd
     if i >= key
-    then Result.ret ret0
+    then Result.ret ret
     else
       do
-        let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
+        let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret
         Result.ret (betree.List.Cons (i, i0) tl0)
-  | betree.List.Nil => Result.ret ret0
+  | betree.List.Nil => Result.ret ret
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
    (there is a single backward function, and the forward function returns ())
@@ -1069,6 +1069,6 @@ def main : Result Unit :=
   Result.ret ()
 
 /- Unit test for [betree_main::main] -/
-#assert (main == .ret ())
+#assert (main == Result.ret ())
 
 end betree_main
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index e5655c7e..48ec6ad5 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -45,7 +45,7 @@ def test_vec : Result Unit :=
     Result.ret ()
 
 /- Unit test for [external::test_vec] -/
-#assert (test_vec == .ret ())
+#assert (test_vec == Result.ret ())
 
 /- [external::custom_swap]: forward function
    Source: 'src/external.rs', lines 24:0-24:66 -/
@@ -60,14 +60,14 @@ def custom_swap
 /- [external::custom_swap]: backward function 0
    Source: 'src/external.rs', lines 24:0-24:66 -/
 def custom_swap_back
-  (T : Type) (x : T) (y : T) (st : State) (ret0 : T) (st0 : State) :
+  (T : Type) (x : T) (y : T) (st : State) (ret : T) (st0 : State) :
   Result (State × (T × T))
   :=
   do
     let (st1, _) ← core.mem.swap T x y st
     let (st2, _) ← core.mem.swap_back0 T x y st st1
     let (_, y0) ← core.mem.swap_back1 T x y st st2
-    Result.ret (st0, (ret0, y0))
+    Result.ret (st0, (ret, y0))
 
 /- [external::test_custom_swap]: forward function
    Source: 'src/external.rs', lines 29:0-29:59 -/
@@ -92,7 +92,7 @@ def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) :=
     let (st0, _) ← swap U32 x 0#u32 st
     let (st1, (x0, _)) ← swap_back U32 x 0#u32 st st0
     if x0 = 0#u32
-    then Result.fail Error.panic
+    then Result.fail .panic
     else Result.ret (st1, x0)
 
 end external
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 95c501f6..e03981a2 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -295,7 +295,7 @@ divergent def HashMap.get_in_list_loop
     if ckey = key
     then Result.ret cvalue
     else HashMap.get_in_list_loop T key tl
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [hashmap::{hashmap::HashMap<T>}::get_in_list]: forward function
    Source: 'src/hashmap.rs', lines 224:4-224:70 -/
@@ -324,7 +324,7 @@ divergent def HashMap.get_mut_in_list_loop
     if ckey = key
     then Result.ret cvalue
     else HashMap.get_mut_in_list_loop T tl key
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: forward function
    Source: 'src/hashmap.rs', lines 245:4-245:86 -/
@@ -335,22 +335,22 @@ def HashMap.get_mut_in_list
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0: backward function 0
    Source: 'src/hashmap.rs', lines 245:4-254:5 -/
 divergent def HashMap.get_mut_in_list_loop_back
-  (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) :=
+  (T : Type) (ls : List T) (key : Usize) (ret : T) : Result (List T) :=
   match ls with
   | List.Cons ckey cvalue tl =>
     if ckey = key
-    then Result.ret (List.Cons ckey ret0 tl)
+    then Result.ret (List.Cons ckey ret tl)
     else
       do
-        let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret0
+        let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret
         Result.ret (List.Cons ckey cvalue tl0)
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: backward function 0
    Source: 'src/hashmap.rs', lines 245:4-245:86 -/
 def HashMap.get_mut_in_list_back
-  (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) :=
-  HashMap.get_mut_in_list_loop_back T ls key ret0
+  (T : Type) (ls : List T) (key : Usize) (ret : T) : Result (List T) :=
+  HashMap.get_mut_in_list_loop_back T ls key ret
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut]: forward function
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
@@ -368,9 +368,7 @@ def HashMap.get_mut (T : Type) (self : HashMap T) (key : Usize) : Result T :=
 /- [hashmap::{hashmap::HashMap<T>}::get_mut]: backward function 0
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
 def HashMap.get_mut_back
-  (T : Type) (self : HashMap T) (key : Usize) (ret0 : T) :
-  Result (HashMap T)
-  :=
+  (T : Type) (self : HashMap T) (key : Usize) (ret : T) : Result (HashMap T) :=
   do
     let hash ← hash_key key
     let i := alloc.vec.Vec.len (List T) self.slots
@@ -379,7 +377,7 @@ def HashMap.get_mut_back
       alloc.vec.Vec.index_mut (List T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots
         hash_mod
-    let l0 ← HashMap.get_mut_in_list_back T l key ret0
+    let l0 ← HashMap.get_mut_in_list_back T l key ret
     let v ←
       alloc.vec.Vec.index_mut_back (List T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots
@@ -397,7 +395,7 @@ divergent def HashMap.remove_from_list_loop
       let mv_ls := core.mem.replace (List T) (List.Cons ckey t tl) List.Nil
       match mv_ls with
       | List.Cons i cvalue tl0 => Result.ret (some cvalue)
-      | List.Nil => Result.fail Error.panic
+      | List.Nil => Result.fail .panic
     else HashMap.remove_from_list_loop T key tl
   | List.Nil => Result.ret none
 
@@ -418,7 +416,7 @@ divergent def HashMap.remove_from_list_loop_back
       let mv_ls := core.mem.replace (List T) (List.Cons ckey t tl) List.Nil
       match mv_ls with
       | List.Cons i cvalue tl0 => Result.ret tl0
-      | List.Nil => Result.fail Error.panic
+      | List.Nil => Result.fail .panic
     else
       do
         let tl0 ← HashMap.remove_from_list_loop_back T key tl
@@ -493,37 +491,37 @@ def test1 : Result Unit :=
     let hm3 ← HashMap.insert U64 hm2 1056#usize 256#u64
     let i ← HashMap.get U64 hm3 128#usize
     if not (i = 18#u64)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else
       do
         let hm4 ← HashMap.get_mut_back U64 hm3 1024#usize 56#u64
         let i0 ← HashMap.get U64 hm4 1024#usize
         if not (i0 = 56#u64)
-        then Result.fail Error.panic
+        then Result.fail .panic
         else
           do
             let x ← HashMap.remove U64 hm4 1024#usize
             match x with
-            | none => Result.fail Error.panic
+            | none => Result.fail .panic
             | some x0 =>
               if not (x0 = 56#u64)
-              then Result.fail Error.panic
+              then Result.fail .panic
               else
                 do
                   let hm5 ← HashMap.remove_back U64 hm4 1024#usize
                   let i1 ← HashMap.get U64 hm5 0#usize
                   if not (i1 = 42#u64)
-                  then Result.fail Error.panic
+                  then Result.fail .panic
                   else
                     do
                       let i2 ← HashMap.get U64 hm5 128#usize
                       if not (i2 = 18#u64)
-                      then Result.fail Error.panic
+                      then Result.fail .panic
                       else
                         do
                           let i3 ← HashMap.get U64 hm5 1056#usize
                           if not (i3 = 256#u64)
-                          then Result.fail Error.panic
+                          then Result.fail .panic
                           else Result.ret ()
 
 end hashmap
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index abe84bbf..f87ad355 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -309,7 +309,7 @@ divergent def hashmap.HashMap.get_in_list_loop
     if ckey = key
     then Result.ret cvalue
     else hashmap.HashMap.get_in_list_loop T key tl
-  | hashmap.List.Nil => Result.fail Error.panic
+  | hashmap.List.Nil => Result.fail .panic
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: forward function
    Source: 'src/hashmap.rs', lines 224:4-224:70 -/
@@ -340,7 +340,7 @@ divergent def hashmap.HashMap.get_mut_in_list_loop
     if ckey = key
     then Result.ret cvalue
     else hashmap.HashMap.get_mut_in_list_loop T tl key
-  | hashmap.List.Nil => Result.fail Error.panic
+  | hashmap.List.Nil => Result.fail .panic
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: forward function
    Source: 'src/hashmap.rs', lines 245:4-245:86 -/
@@ -351,26 +351,26 @@ def hashmap.HashMap.get_mut_in_list
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0: backward function 0
    Source: 'src/hashmap.rs', lines 245:4-254:5 -/
 divergent def hashmap.HashMap.get_mut_in_list_loop_back
-  (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) :
+  (T : Type) (ls : hashmap.List T) (key : Usize) (ret : T) :
   Result (hashmap.List T)
   :=
   match ls with
   | hashmap.List.Cons ckey cvalue tl =>
     if ckey = key
-    then Result.ret (hashmap.List.Cons ckey ret0 tl)
+    then Result.ret (hashmap.List.Cons ckey ret tl)
     else
       do
-        let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret0
+        let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret
         Result.ret (hashmap.List.Cons ckey cvalue tl0)
-  | hashmap.List.Nil => Result.fail Error.panic
+  | hashmap.List.Nil => Result.fail .panic
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: backward function 0
    Source: 'src/hashmap.rs', lines 245:4-245:86 -/
 def hashmap.HashMap.get_mut_in_list_back
-  (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) :
+  (T : Type) (ls : hashmap.List T) (key : Usize) (ret : T) :
   Result (hashmap.List T)
   :=
-  hashmap.HashMap.get_mut_in_list_loop_back T ls key ret0
+  hashmap.HashMap.get_mut_in_list_loop_back T ls key ret
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: forward function
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
@@ -389,7 +389,7 @@ def hashmap.HashMap.get_mut
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: backward function 0
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
 def hashmap.HashMap.get_mut_back
-  (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret0 : T) :
+  (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret : T) :
   Result (hashmap.HashMap T)
   :=
   do
@@ -400,7 +400,7 @@ def hashmap.HashMap.get_mut_back
       alloc.vec.Vec.index_mut (hashmap.List T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T))
         self.slots hash_mod
-    let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0
+    let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret
     let v ←
       alloc.vec.Vec.index_mut_back (hashmap.List T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T))
@@ -420,7 +420,7 @@ divergent def hashmap.HashMap.remove_from_list_loop
           hashmap.List.Nil
       match mv_ls with
       | hashmap.List.Cons i cvalue tl0 => Result.ret (some cvalue)
-      | hashmap.List.Nil => Result.fail Error.panic
+      | hashmap.List.Nil => Result.fail .panic
     else hashmap.HashMap.remove_from_list_loop T key tl
   | hashmap.List.Nil => Result.ret none
 
@@ -443,7 +443,7 @@ divergent def hashmap.HashMap.remove_from_list_loop_back
           hashmap.List.Nil
       match mv_ls with
       | hashmap.List.Cons i cvalue tl0 => Result.ret tl0
-      | hashmap.List.Nil => Result.fail Error.panic
+      | hashmap.List.Nil => Result.fail .panic
     else
       do
         let tl0 ← hashmap.HashMap.remove_from_list_loop_back T key tl
@@ -520,37 +520,37 @@ def hashmap.test1 : Result Unit :=
     let hm3 ← hashmap.HashMap.insert U64 hm2 1056#usize 256#u64
     let i ← hashmap.HashMap.get U64 hm3 128#usize
     if not (i = 18#u64)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else
       do
         let hm4 ← hashmap.HashMap.get_mut_back U64 hm3 1024#usize 56#u64
         let i0 ← hashmap.HashMap.get U64 hm4 1024#usize
         if not (i0 = 56#u64)
-        then Result.fail Error.panic
+        then Result.fail .panic
         else
           do
             let x ← hashmap.HashMap.remove U64 hm4 1024#usize
             match x with
-            | none => Result.fail Error.panic
+            | none => Result.fail .panic
             | some x0 =>
               if not (x0 = 56#u64)
-              then Result.fail Error.panic
+              then Result.fail .panic
               else
                 do
                   let hm5 ← hashmap.HashMap.remove_back U64 hm4 1024#usize
                   let i1 ← hashmap.HashMap.get U64 hm5 0#usize
                   if not (i1 = 42#u64)
-                  then Result.fail Error.panic
+                  then Result.fail .panic
                   else
                     do
                       let i2 ← hashmap.HashMap.get U64 hm5 128#usize
                       if not (i2 = 18#u64)
-                      then Result.fail Error.panic
+                      then Result.fail .panic
                       else
                         do
                           let i3 ← hashmap.HashMap.get U64 hm5 1056#usize
                           if not (i3 = 256#u64)
-                          then Result.fail Error.panic
+                          then Result.fail .panic
                           else Result.ret ()
 
 /- [hashmap_main::insert_on_disk]: forward function
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index ae1d87aa..08aa08a5 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -107,7 +107,7 @@ divergent def list_nth_mut_loop_loop
     else do
            let i0 ← i - 1#u32
            list_nth_mut_loop_loop T tl i0
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop]: forward function
    Source: 'src/loops.rs', lines 78:0-78:71 -/
@@ -117,23 +117,23 @@ def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T :=
 /- [loops::list_nth_mut_loop]: loop 0: backward function 0
    Source: 'src/loops.rs', lines 78:0-88:1 -/
 divergent def list_nth_mut_loop_loop_back
-  (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
+  (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) :=
   match ls with
   | List.Cons x tl =>
     if i = 0#u32
-    then Result.ret (List.Cons ret0 tl)
+    then Result.ret (List.Cons ret tl)
     else
       do
         let i0 ← i - 1#u32
-        let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
+        let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret
         Result.ret (List.Cons x tl0)
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop]: backward function 0
    Source: 'src/loops.rs', lines 78:0-78:71 -/
 def list_nth_mut_loop_back
-  (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
-  list_nth_mut_loop_loop_back T ls i ret0
+  (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) :=
+  list_nth_mut_loop_loop_back T ls i ret
 
 /- [loops::list_nth_shared_loop]: loop 0: forward function
    Source: 'src/loops.rs', lines 91:0-101:1 -/
@@ -146,7 +146,7 @@ divergent def list_nth_shared_loop_loop
     else do
            let i0 ← i - 1#u32
            list_nth_shared_loop_loop T tl i0
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_loop]: forward function
    Source: 'src/loops.rs', lines 91:0-91:66 -/
@@ -160,7 +160,7 @@ divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize :=
   | List.Cons y tl => if y = x
                       then Result.ret y
                       else get_elem_mut_loop x tl
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::get_elem_mut]: forward function
    Source: 'src/loops.rs', lines 103:0-103:73 -/
@@ -175,28 +175,28 @@ def get_elem_mut
 /- [loops::get_elem_mut]: loop 0: backward function 0
    Source: 'src/loops.rs', lines 103:0-117:1 -/
 divergent def get_elem_mut_loop_back
-  (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) :=
+  (x : Usize) (ls : List Usize) (ret : Usize) : Result (List Usize) :=
   match ls with
   | List.Cons y tl =>
     if y = x
-    then Result.ret (List.Cons ret0 tl)
+    then Result.ret (List.Cons ret tl)
     else
       do
-        let tl0 ← get_elem_mut_loop_back x tl ret0
+        let tl0 ← get_elem_mut_loop_back x tl ret
         Result.ret (List.Cons y tl0)
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::get_elem_mut]: backward function 0
    Source: 'src/loops.rs', lines 103:0-103:73 -/
 def get_elem_mut_back
-  (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret0 : Usize) :
+  (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret : Usize) :
   Result (alloc.vec.Vec (List Usize))
   :=
   do
     let l ←
       alloc.vec.Vec.index_mut (List Usize) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
-    let l0 ← get_elem_mut_loop_back x l ret0
+    let l0 ← get_elem_mut_loop_back x l ret
     alloc.vec.Vec.index_mut_back (List Usize) Usize
       (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
       l0
@@ -209,7 +209,7 @@ divergent def get_elem_shared_loop
   | List.Cons y tl => if y = x
                       then Result.ret y
                       else get_elem_shared_loop x tl
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::get_elem_shared]: forward function
    Source: 'src/loops.rs', lines 119:0-119:68 -/
@@ -228,8 +228,8 @@ def id_mut (T : Type) (ls : List T) : Result (List T) :=
 
 /- [loops::id_mut]: backward function 0
    Source: 'src/loops.rs', lines 135:0-135:50 -/
-def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) :=
-  Result.ret ret0
+def id_mut_back (T : Type) (ls : List T) (ret : List T) : Result (List T) :=
+  Result.ret ret
 
 /- [loops::id_shared]: forward function
    Source: 'src/loops.rs', lines 139:0-139:45 -/
@@ -247,7 +247,7 @@ divergent def list_nth_mut_loop_with_id_loop
     else do
            let i0 ← i - 1#u32
            list_nth_mut_loop_with_id_loop T i0 tl
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_with_id]: forward function
    Source: 'src/loops.rs', lines 144:0-144:75 -/
@@ -259,25 +259,25 @@ def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T :=
 /- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0
    Source: 'src/loops.rs', lines 144:0-155:1 -/
 divergent def list_nth_mut_loop_with_id_loop_back
-  (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) :=
+  (T : Type) (i : U32) (ls : List T) (ret : T) : Result (List T) :=
   match ls with
   | List.Cons x tl =>
     if i = 0#u32
-    then Result.ret (List.Cons ret0 tl)
+    then Result.ret (List.Cons ret tl)
     else
       do
         let i0 ← i - 1#u32
-        let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
+        let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret
         Result.ret (List.Cons x tl0)
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_with_id]: backward function 0
    Source: 'src/loops.rs', lines 144:0-144:75 -/
 def list_nth_mut_loop_with_id_back
-  (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
+  (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) :=
   do
     let ls0 ← id_mut T ls
-    let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0
+    let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret
     id_mut_back T ls l
 
 /- [loops::list_nth_shared_loop_with_id]: loop 0: forward function
@@ -291,7 +291,7 @@ divergent def list_nth_shared_loop_with_id_loop
     else do
            let i0 ← i - 1#u32
            list_nth_shared_loop_with_id_loop T i0 tl
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_loop_with_id]: forward function
    Source: 'src/loops.rs', lines 158:0-158:70 -/
@@ -314,8 +314,8 @@ divergent def list_nth_mut_loop_pair_loop
       else do
              let i0 ← i - 1#u32
              list_nth_mut_loop_pair_loop T tl0 tl1 i0
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_pair]: forward function
    Source: 'src/loops.rs', lines 174:0-178:27 -/
@@ -326,7 +326,7 @@ def list_nth_mut_loop_pair
 /- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0
    Source: 'src/loops.rs', lines 174:0-195:1 -/
 divergent def list_nth_mut_loop_pair_loop_back'a
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
   match ls0 with
@@ -334,27 +334,27 @@ divergent def list_nth_mut_loop_pair_loop_back'a
     match ls1 with
     | List.Cons x1 tl1 =>
       if i = 0#u32
-      then Result.ret (List.Cons ret0 tl0)
+      then Result.ret (List.Cons ret tl0)
       else
         do
           let i0 ← i - 1#u32
-          let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
+          let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret
           Result.ret (List.Cons x0 tl00)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_pair]: backward function 0
    Source: 'src/loops.rs', lines 174:0-178:27 -/
 def list_nth_mut_loop_pair_back'a
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
-  list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0
+  list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret
 
 /- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1
    Source: 'src/loops.rs', lines 174:0-195:1 -/
 divergent def list_nth_mut_loop_pair_loop_back'b
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
   match ls0 with
@@ -362,22 +362,22 @@ divergent def list_nth_mut_loop_pair_loop_back'b
     match ls1 with
     | List.Cons x1 tl1 =>
       if i = 0#u32
-      then Result.ret (List.Cons ret0 tl1)
+      then Result.ret (List.Cons ret tl1)
       else
         do
           let i0 ← i - 1#u32
-          let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
+          let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret
           Result.ret (List.Cons x1 tl10)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_pair]: backward function 1
    Source: 'src/loops.rs', lines 174:0-178:27 -/
 def list_nth_mut_loop_pair_back'b
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
-  list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0
+  list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret
 
 /- [loops::list_nth_shared_loop_pair]: loop 0: forward function
    Source: 'src/loops.rs', lines 198:0-219:1 -/
@@ -392,8 +392,8 @@ divergent def list_nth_shared_loop_pair_loop
       else do
              let i0 ← i - 1#u32
              list_nth_shared_loop_pair_loop T tl0 tl1 i0
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_loop_pair]: forward function
    Source: 'src/loops.rs', lines 198:0-202:19 -/
@@ -415,8 +415,8 @@ divergent def list_nth_mut_loop_pair_merge_loop
         do
           let i0 ← i - 1#u32
           list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_pair_merge]: forward function
    Source: 'src/loops.rs', lines 223:0-227:27 -/
@@ -427,7 +427,7 @@ def list_nth_mut_loop_pair_merge
 /- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0
    Source: 'src/loops.rs', lines 223:0-238:1 -/
 divergent def list_nth_mut_loop_pair_merge_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : (T × T)) :
   Result ((List T) × (List T))
   :=
   match ls0 with
@@ -435,24 +435,24 @@ divergent def list_nth_mut_loop_pair_merge_loop_back
     match ls1 with
     | List.Cons x1 tl1 =>
       if i = 0#u32
-      then let (t, t0) := ret0
+      then let (t, t0) := ret
            Result.ret (List.Cons t tl0, List.Cons t0 tl1)
       else
         do
           let i0 ← i - 1#u32
           let (tl00, tl10) ←
-            list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+            list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret
           Result.ret (List.Cons x0 tl00, List.Cons x1 tl10)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_pair_merge]: backward function 0
    Source: 'src/loops.rs', lines 223:0-227:27 -/
 def list_nth_mut_loop_pair_merge_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : (T × T)) :
   Result ((List T) × (List T))
   :=
-  list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
+  list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret
 
 /- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function
    Source: 'src/loops.rs', lines 241:0-256:1 -/
@@ -468,8 +468,8 @@ divergent def list_nth_shared_loop_pair_merge_loop
         do
           let i0 ← i - 1#u32
           list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_loop_pair_merge]: forward function
    Source: 'src/loops.rs', lines 241:0-245:19 -/
@@ -491,8 +491,8 @@ divergent def list_nth_mut_shared_loop_pair_loop
         do
           let i0 ← i - 1#u32
           list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_shared_loop_pair]: forward function
    Source: 'src/loops.rs', lines 259:0-263:23 -/
@@ -503,7 +503,7 @@ def list_nth_mut_shared_loop_pair
 /- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0
    Source: 'src/loops.rs', lines 259:0-274:1 -/
 divergent def list_nth_mut_shared_loop_pair_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
   match ls0 with
@@ -511,23 +511,22 @@ divergent def list_nth_mut_shared_loop_pair_loop_back
     match ls1 with
     | List.Cons x1 tl1 =>
       if i = 0#u32
-      then Result.ret (List.Cons ret0 tl0)
+      then Result.ret (List.Cons ret tl0)
       else
         do
           let i0 ← i - 1#u32
-          let tl00 ←
-            list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
+          let tl00 ← list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret
           Result.ret (List.Cons x0 tl00)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_shared_loop_pair]: backward function 0
    Source: 'src/loops.rs', lines 259:0-263:23 -/
 def list_nth_mut_shared_loop_pair_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
-  list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0
+  list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function
    Source: 'src/loops.rs', lines 278:0-293:1 -/
@@ -543,8 +542,8 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
         do
           let i0 ← i - 1#u32
           list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]: forward function
    Source: 'src/loops.rs', lines 278:0-282:23 -/
@@ -555,7 +554,7 @@ def list_nth_mut_shared_loop_pair_merge
 /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0
    Source: 'src/loops.rs', lines 278:0-293:1 -/
 divergent def list_nth_mut_shared_loop_pair_merge_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
   match ls0 with
@@ -563,23 +562,23 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back
     match ls1 with
     | List.Cons x1 tl1 =>
       if i = 0#u32
-      then Result.ret (List.Cons ret0 tl0)
+      then Result.ret (List.Cons ret tl0)
       else
         do
           let i0 ← i - 1#u32
           let tl00 ←
-            list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+            list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret
           Result.ret (List.Cons x0 tl00)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0
    Source: 'src/loops.rs', lines 278:0-282:23 -/
 def list_nth_mut_shared_loop_pair_merge_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
-  list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0
+  list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret
 
 /- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function
    Source: 'src/loops.rs', lines 297:0-312:1 -/
@@ -595,8 +594,8 @@ divergent def list_nth_shared_mut_loop_pair_loop
         do
           let i0 ← i - 1#u32
           list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_mut_loop_pair]: forward function
    Source: 'src/loops.rs', lines 297:0-301:23 -/
@@ -607,7 +606,7 @@ def list_nth_shared_mut_loop_pair
 /- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1
    Source: 'src/loops.rs', lines 297:0-312:1 -/
 divergent def list_nth_shared_mut_loop_pair_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
   match ls0 with
@@ -615,23 +614,22 @@ divergent def list_nth_shared_mut_loop_pair_loop_back
     match ls1 with
     | List.Cons x1 tl1 =>
       if i = 0#u32
-      then Result.ret (List.Cons ret0 tl1)
+      then Result.ret (List.Cons ret tl1)
       else
         do
           let i0 ← i - 1#u32
-          let tl10 ←
-            list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
+          let tl10 ← list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret
           Result.ret (List.Cons x1 tl10)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_mut_loop_pair]: backward function 1
    Source: 'src/loops.rs', lines 297:0-301:23 -/
 def list_nth_shared_mut_loop_pair_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
-  list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0
+  list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function
    Source: 'src/loops.rs', lines 316:0-331:1 -/
@@ -647,8 +645,8 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
         do
           let i0 ← i - 1#u32
           list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]: forward function
    Source: 'src/loops.rs', lines 316:0-320:23 -/
@@ -659,7 +657,7 @@ def list_nth_shared_mut_loop_pair_merge
 /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0
    Source: 'src/loops.rs', lines 316:0-331:1 -/
 divergent def list_nth_shared_mut_loop_pair_merge_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
   match ls0 with
@@ -667,22 +665,22 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back
     match ls1 with
     | List.Cons x1 tl1 =>
       if i = 0#u32
-      then Result.ret (List.Cons ret0 tl1)
+      then Result.ret (List.Cons ret tl1)
       else
         do
           let i0 ← i - 1#u32
           let tl10 ←
-            list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+            list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret
           Result.ret (List.Cons x1 tl10)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail .panic
+  | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0
    Source: 'src/loops.rs', lines 316:0-320:23 -/
 def list_nth_shared_mut_loop_pair_merge_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
   Result (List T)
   :=
-  list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
+  list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret
 
 end loops
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 3b1c3f9f..ca66c628 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -101,7 +101,7 @@ def test2 : Result Unit :=
     Result.ret ()
 
 /- Unit test for [no_nested_borrows::test2] -/
-#assert (test2 == .ret ())
+#assert (test2 == Result.ret ())
 
 /- [no_nested_borrows::get_max]: forward function
    Source: 'src/no_nested_borrows.rs', lines 111:0-111:37 -/
@@ -118,11 +118,11 @@ def test3 : Result Unit :=
     let y ← get_max 10#u32 11#u32
     let z ← x + y
     if not (z = 15#u32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else Result.ret ()
 
 /- Unit test for [no_nested_borrows::test3] -/
-#assert (test3 == .ret ())
+#assert (test3 == Result.ret ())
 
 /- [no_nested_borrows::test_neg1]: forward function
    Source: 'src/no_nested_borrows.rs', lines 126:0-126:18 -/
@@ -130,40 +130,39 @@ def test_neg1 : Result Unit :=
   do
     let y ← - 3#i32
     if not (y = (-(3:Int))#i32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_neg1] -/
-#assert (test_neg1 == .ret ())
+#assert (test_neg1 == Result.ret ())
 
 /- [no_nested_borrows::refs_test1]: forward function
    Source: 'src/no_nested_borrows.rs', lines 133:0-133:19 -/
 def refs_test1 : Result Unit :=
   if not (1#i32 = 1#i32)
-  then Result.fail Error.panic
+  then Result.fail .panic
   else Result.ret ()
 
 /- Unit test for [no_nested_borrows::refs_test1] -/
-#assert (refs_test1 == .ret ())
+#assert (refs_test1 == Result.ret ())
 
 /- [no_nested_borrows::refs_test2]: forward function
    Source: 'src/no_nested_borrows.rs', lines 144:0-144:19 -/
 def refs_test2 : Result Unit :=
   if not (2#i32 = 2#i32)
-  then Result.fail Error.panic
+  then Result.fail .panic
   else
     if not (0#i32 = 0#i32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else
       if not (2#i32 = 2#i32)
-      then Result.fail Error.panic
-      else
-        if not (2#i32 = 2#i32)
-        then Result.fail Error.panic
-        else Result.ret ()
+      then Result.fail .panic
+      else if not (2#i32 = 2#i32)
+           then Result.fail .panic
+           else Result.ret ()
 
 /- Unit test for [no_nested_borrows::refs_test2] -/
-#assert (refs_test2 == .ret ())
+#assert (refs_test2 == Result.ret ())
 
 /- [no_nested_borrows::test_list1]: forward function
    Source: 'src/no_nested_borrows.rs', lines 160:0-160:19 -/
@@ -171,7 +170,7 @@ def test_list1 : Result Unit :=
   Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_list1] -/
-#assert (test_list1 == .ret ())
+#assert (test_list1 == Result.ret ())
 
 /- [no_nested_borrows::test_box1]: forward function
    Source: 'src/no_nested_borrows.rs', lines 165:0-165:18 -/
@@ -181,11 +180,11 @@ def test_box1 : Result Unit :=
     let b0 ← alloc.boxed.Box.deref_mut_back I32 b 1#i32
     let x ← alloc.boxed.Box.deref I32 b0
     if not (x = 1#i32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_box1] -/
-#assert (test_box1 == .ret ())
+#assert (test_box1 == Result.ret ())
 
 /- [no_nested_borrows::copy_int]: forward function
    Source: 'src/no_nested_borrows.rs', lines 175:0-175:30 -/
@@ -196,14 +195,14 @@ def copy_int (x : I32) : Result I32 :=
    Source: 'src/no_nested_borrows.rs', lines 181:0-181:32 -/
 def test_unreachable (b : Bool) : Result Unit :=
   if b
-  then Result.fail Error.panic
+  then Result.fail .panic
   else Result.ret ()
 
 /- [no_nested_borrows::test_panic]: forward function
    Source: 'src/no_nested_borrows.rs', lines 189:0-189:26 -/
 def test_panic (b : Bool) : Result Unit :=
   if b
-  then Result.fail Error.panic
+  then Result.fail .panic
   else Result.ret ()
 
 /- [no_nested_borrows::test_copy_int]: forward function
@@ -212,11 +211,11 @@ def test_copy_int : Result Unit :=
   do
     let y ← copy_int 0#i32
     if not (0#i32 = y)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_copy_int] -/
-#assert (test_copy_int == .ret ())
+#assert (test_copy_int == Result.ret ())
 
 /- [no_nested_borrows::is_cons]: forward function
    Source: 'src/no_nested_borrows.rs', lines 203:0-203:38 -/
@@ -232,18 +231,18 @@ def test_is_cons : Result Unit :=
     let l := List.Nil
     let b ← is_cons I32 (List.Cons 0#i32 l)
     if not b
-    then Result.fail Error.panic
+    then Result.fail .panic
     else Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_is_cons] -/
-#assert (test_is_cons == .ret ())
+#assert (test_is_cons == Result.ret ())
 
 /- [no_nested_borrows::split_list]: forward function
    Source: 'src/no_nested_borrows.rs', lines 216:0-216:48 -/
 def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
   match l with
   | List.Cons hd tl => Result.ret (hd, tl)
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::test_split_list]: forward function
    Source: 'src/no_nested_borrows.rs', lines 224:0-224:24 -/
@@ -253,11 +252,11 @@ def test_split_list : Result Unit :=
     let p ← split_list I32 (List.Cons 0#i32 l)
     let (hd, _) := p
     if not (hd = 0#i32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_split_list] -/
-#assert (test_split_list == .ret ())
+#assert (test_split_list == Result.ret ())
 
 /- [no_nested_borrows::choose]: forward function
    Source: 'src/no_nested_borrows.rs', lines 231:0-231:70 -/
@@ -269,10 +268,10 @@ def choose (T : Type) (b : Bool) (x : T) (y : T) : Result T :=
 /- [no_nested_borrows::choose]: backward function 0
    Source: 'src/no_nested_borrows.rs', lines 231:0-231:70 -/
 def choose_back
-  (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) :=
+  (T : Type) (b : Bool) (x : T) (y : T) (ret : T) : Result (T × T) :=
   if b
-  then Result.ret (ret0, y)
-  else Result.ret (x, ret0)
+  then Result.ret (ret, y)
+  else Result.ret (x, ret)
 
 /- [no_nested_borrows::choose_test]: forward function
    Source: 'src/no_nested_borrows.rs', lines 239:0-239:20 -/
@@ -281,18 +280,18 @@ def choose_test : Result Unit :=
     let z ← choose I32 true 0#i32 0#i32
     let z0 ← z + 1#i32
     if not (z0 = 1#i32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else
       do
         let (x, y) ← choose_back I32 true 0#i32 0#i32 z0
         if not (x = 1#i32)
-        then Result.fail Error.panic
+        then Result.fail .panic
         else if not (y = 0#i32)
-             then Result.fail Error.panic
+             then Result.fail .panic
              else Result.ret ()
 
 /- Unit test for [no_nested_borrows::choose_test] -/
-#assert (choose_test == .ret ())
+#assert (choose_test == Result.ret ())
 
 /- [no_nested_borrows::test_char]: forward function
    Source: 'src/no_nested_borrows.rs', lines 251:0-251:26 -/
@@ -334,7 +333,7 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
     else do
            let i0 ← i - 1#u32
            list_nth_shared T tl i0
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::list_nth_mut]: forward function
    Source: 'src/no_nested_borrows.rs', lines 320:0-320:67 -/
@@ -346,22 +345,22 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
     else do
            let i0 ← i - 1#u32
            list_nth_mut T tl i0
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::list_nth_mut]: backward function 0
    Source: 'src/no_nested_borrows.rs', lines 320:0-320:67 -/
 divergent def list_nth_mut_back
-  (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
+  (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) :=
   match l with
   | List.Cons x tl =>
     if i = 0#u32
-    then Result.ret (List.Cons ret0 tl)
+    then Result.ret (List.Cons ret tl)
     else
       do
         let i0 ← i - 1#u32
-        let tl0 ← list_nth_mut_back T tl i0 ret0
+        let tl0 ← list_nth_mut_back T tl i0 ret
         Result.ret (List.Cons x tl0)
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::list_rev_aux]: forward function
    Source: 'src/no_nested_borrows.rs', lines 336:0-336:63 -/
@@ -387,43 +386,43 @@ def test_list_functions : Result Unit :=
     let l1 := List.Cons 1#i32 l0
     let i ← list_length I32 (List.Cons 0#i32 l1)
     if not (i = 3#u32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else
       do
         let i0 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32
         if not (i0 = 0#i32)
-        then Result.fail Error.panic
+        then Result.fail .panic
         else
           do
             let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32
             if not (i1 = 1#i32)
-            then Result.fail Error.panic
+            then Result.fail .panic
             else
               do
                 let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32
                 if not (i2 = 2#i32)
-                then Result.fail Error.panic
+                then Result.fail .panic
                 else
                   do
                     let ls ←
                       list_nth_mut_back I32 (List.Cons 0#i32 l1) 1#u32 3#i32
                     let i3 ← list_nth_shared I32 ls 0#u32
                     if not (i3 = 0#i32)
-                    then Result.fail Error.panic
+                    then Result.fail .panic
                     else
                       do
                         let i4 ← list_nth_shared I32 ls 1#u32
                         if not (i4 = 3#i32)
-                        then Result.fail Error.panic
+                        then Result.fail .panic
                         else
                           do
                             let i5 ← list_nth_shared I32 ls 2#u32
                             if not (i5 = 2#i32)
-                            then Result.fail Error.panic
+                            then Result.fail .panic
                             else Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_list_functions] -/
-#assert (test_list_functions == .ret ())
+#assert (test_list_functions == Result.ret ())
 
 /- [no_nested_borrows::id_mut_pair1]: forward function
    Source: 'src/no_nested_borrows.rs', lines 371:0-371:89 -/
@@ -433,8 +432,8 @@ def id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : Result (T1 × T2) :=
 /- [no_nested_borrows::id_mut_pair1]: backward function 0
    Source: 'src/no_nested_borrows.rs', lines 371:0-371:89 -/
 def id_mut_pair1_back
-  (T1 T2 : Type) (x : T1) (y : T2) (ret0 : (T1 × T2)) : Result (T1 × T2) :=
-  let (t, t0) := ret0
+  (T1 T2 : Type) (x : T1) (y : T2) (ret : (T1 × T2)) : Result (T1 × T2) :=
+  let (t, t0) := ret
   Result.ret (t, t0)
 
 /- [no_nested_borrows::id_mut_pair2]: forward function
@@ -446,8 +445,8 @@ def id_mut_pair2 (T1 T2 : Type) (p : (T1 × T2)) : Result (T1 × T2) :=
 /- [no_nested_borrows::id_mut_pair2]: backward function 0
    Source: 'src/no_nested_borrows.rs', lines 375:0-375:88 -/
 def id_mut_pair2_back
-  (T1 T2 : Type) (p : (T1 × T2)) (ret0 : (T1 × T2)) : Result (T1 × T2) :=
-  let (t, t0) := ret0
+  (T1 T2 : Type) (p : (T1 × T2)) (ret : (T1 × T2)) : Result (T1 × T2) :=
+  let (t, t0) := ret
   Result.ret (t, t0)
 
 /- [no_nested_borrows::id_mut_pair3]: forward function
@@ -458,14 +457,14 @@ def id_mut_pair3 (T1 T2 : Type) (x : T1) (y : T2) : Result (T1 × T2) :=
 /- [no_nested_borrows::id_mut_pair3]: backward function 0
    Source: 'src/no_nested_borrows.rs', lines 379:0-379:93 -/
 def id_mut_pair3_back'a
-  (T1 T2 : Type) (x : T1) (y : T2) (ret0 : T1) : Result T1 :=
-  Result.ret ret0
+  (T1 T2 : Type) (x : T1) (y : T2) (ret : T1) : Result T1 :=
+  Result.ret ret
 
 /- [no_nested_borrows::id_mut_pair3]: backward function 1
    Source: 'src/no_nested_borrows.rs', lines 379:0-379:93 -/
 def id_mut_pair3_back'b
-  (T1 T2 : Type) (x : T1) (y : T2) (ret0 : T2) : Result T2 :=
-  Result.ret ret0
+  (T1 T2 : Type) (x : T1) (y : T2) (ret : T2) : Result T2 :=
+  Result.ret ret
 
 /- [no_nested_borrows::id_mut_pair4]: forward function
    Source: 'src/no_nested_borrows.rs', lines 383:0-383:92 -/
@@ -476,14 +475,14 @@ def id_mut_pair4 (T1 T2 : Type) (p : (T1 × T2)) : Result (T1 × T2) :=
 /- [no_nested_borrows::id_mut_pair4]: backward function 0
    Source: 'src/no_nested_borrows.rs', lines 383:0-383:92 -/
 def id_mut_pair4_back'a
-  (T1 T2 : Type) (p : (T1 × T2)) (ret0 : T1) : Result T1 :=
-  Result.ret ret0
+  (T1 T2 : Type) (p : (T1 × T2)) (ret : T1) : Result T1 :=
+  Result.ret ret
 
 /- [no_nested_borrows::id_mut_pair4]: backward function 1
    Source: 'src/no_nested_borrows.rs', lines 383:0-383:92 -/
 def id_mut_pair4_back'b
-  (T1 T2 : Type) (p : (T1 × T2)) (ret0 : T2) : Result T2 :=
-  Result.ret ret0
+  (T1 T2 : Type) (p : (T1 × T2)) (ret : T2) : Result T2 :=
+  Result.ret ret
 
 /- [no_nested_borrows::StructWithTuple]
    Source: 'src/no_nested_borrows.rs', lines 390:0-390:34 -/
@@ -522,28 +521,28 @@ def test_constants : Result Unit :=
     let swt ← new_tuple1
     let (i, _) := swt.p
     if not (i = 1#u32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else
       do
         let swt0 ← new_tuple2
         let (i0, _) := swt0.p
         if not (i0 = 1#i16)
-        then Result.fail Error.panic
+        then Result.fail .panic
         else
           do
             let swt1 ← new_tuple3
             let (i1, _) := swt1.p
             if not (i1 = 1#u64)
-            then Result.fail Error.panic
+            then Result.fail .panic
             else
               do
                 let swp ← new_pair1
                 if not (swp.p.x = 1#u32)
-                then Result.fail Error.panic
+                then Result.fail .panic
                 else Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_constants] -/
-#assert (test_constants == .ret ())
+#assert (test_constants == Result.ret ())
 
 /- [no_nested_borrows::test_weird_borrows1]: forward function
    Source: 'src/no_nested_borrows.rs', lines 428:0-428:28 -/
@@ -551,7 +550,7 @@ def test_weird_borrows1 : Result Unit :=
   Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_weird_borrows1] -/
-#assert (test_weird_borrows1 == .ret ())
+#assert (test_weird_borrows1 == Result.ret ())
 
 /- [no_nested_borrows::test_mem_replace]: merged forward/backward function
    (there is a single backward function, and the forward function returns ())
@@ -559,7 +558,7 @@ def test_weird_borrows1 : Result Unit :=
 def test_mem_replace (px : U32) : Result U32 :=
   let y := core.mem.replace U32 px 1#u32
   if not (y = 0#u32)
-  then Result.fail Error.panic
+  then Result.fail .panic
   else Result.ret 2#u32
 
 /- [no_nested_borrows::test_shared_borrow_bool1]: forward function
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 37e0e70e..08386bb7 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -17,11 +17,11 @@ def test_incr : Result Unit :=
   do
     let x ← ref_incr 0#i32
     if not (x = 1#i32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else Result.ret ()
 
 /- Unit test for [paper::test_incr] -/
-#assert (test_incr == .ret ())
+#assert (test_incr == Result.ret ())
 
 /- [paper::choose]: forward function
    Source: 'src/paper.rs', lines 15:0-15:70 -/
@@ -33,10 +33,10 @@ def choose (T : Type) (b : Bool) (x : T) (y : T) : Result T :=
 /- [paper::choose]: backward function 0
    Source: 'src/paper.rs', lines 15:0-15:70 -/
 def choose_back
-  (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) :=
+  (T : Type) (b : Bool) (x : T) (y : T) (ret : T) : Result (T × T) :=
   if b
-  then Result.ret (ret0, y)
-  else Result.ret (x, ret0)
+  then Result.ret (ret, y)
+  else Result.ret (x, ret)
 
 /- [paper::test_choose]: forward function
    Source: 'src/paper.rs', lines 23:0-23:20 -/
@@ -45,18 +45,18 @@ def test_choose : Result Unit :=
     let z ← choose I32 true 0#i32 0#i32
     let z0 ← z + 1#i32
     if not (z0 = 1#i32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else
       do
         let (x, y) ← choose_back I32 true 0#i32 0#i32 z0
         if not (x = 1#i32)
-        then Result.fail Error.panic
+        then Result.fail .panic
         else if not (y = 0#i32)
-             then Result.fail Error.panic
+             then Result.fail .panic
              else Result.ret ()
 
 /- Unit test for [paper::test_choose] -/
-#assert (test_choose == .ret ())
+#assert (test_choose == Result.ret ())
 
 /- [paper::List]
    Source: 'src/paper.rs', lines 35:0-35:16 -/
@@ -74,22 +74,22 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
     else do
            let i0 ← i - 1#u32
            list_nth_mut T tl i0
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [paper::list_nth_mut]: backward function 0
    Source: 'src/paper.rs', lines 42:0-42:67 -/
 divergent def list_nth_mut_back
-  (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
+  (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) :=
   match l with
   | List.Cons x tl =>
     if i = 0#u32
-    then Result.ret (List.Cons ret0 tl)
+    then Result.ret (List.Cons ret tl)
     else
       do
         let i0 ← i - 1#u32
-        let tl0 ← list_nth_mut_back T tl i0 ret0
+        let tl0 ← list_nth_mut_back T tl i0 ret
         Result.ret (List.Cons x tl0)
-  | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail .panic
 
 /- [paper::sum]: forward function
    Source: 'src/paper.rs', lines 57:0-57:32 -/
@@ -112,11 +112,11 @@ def test_nth : Result Unit :=
     let l2 ← list_nth_mut_back I32 (List.Cons 1#i32 l1) 2#u32 x0
     let i ← sum l2
     if not (i = 7#i32)
-    then Result.fail Error.panic
+    then Result.fail .panic
     else Result.ret ()
 
 /- Unit test for [paper::test_nth] -/
-#assert (test_nth == .ret ())
+#assert (test_nth == Result.ret ())
 
 /- [paper::call_choose]: forward function
    Source: 'src/paper.rs', lines 76:0-76:44 -/
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 0ef71791..37f0dffb 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -24,15 +24,15 @@ divergent def get_list_at_x (ls : List U32) (x : U32) : Result (List U32) :=
 /- [polonius_list::get_list_at_x]: backward function 0
    Source: 'src/polonius_list.rs', lines 13:0-13:76 -/
 divergent def get_list_at_x_back
-  (ls : List U32) (x : U32) (ret0 : List U32) : Result (List U32) :=
+  (ls : List U32) (x : U32) (ret : List U32) : Result (List U32) :=
   match ls with
   | List.Cons hd tl =>
     if hd = x
-    then Result.ret ret0
+    then Result.ret ret
     else
       do
-        let tl0 ← get_list_at_x_back tl x ret0
+        let tl0 ← get_list_at_x_back tl x ret
         Result.ret (List.Cons hd tl0)
-  | List.Nil => Result.ret ret0
+  | List.Nil => Result.ret ret
 
 end polonius_list
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 9ac4736c..e7795d9c 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -326,15 +326,11 @@ def test_where2
   :=
   Result.ret ()
 
-/- [alloc::string::String]
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 -/
-axiom alloc.string.String : Type
-
 /- Trait declaration: [traits::ParentTrait0]
    Source: 'src/traits.rs', lines 200:0-200:22 -/
 structure ParentTrait0 (Self : Type) where
   W : Type
-  get_name : Self → Result alloc.string.String
+  get_name : Self → Result String
   get_w : Self → Result W
 
 /- Trait declaration: [traits::ParentTrait1]
@@ -350,9 +346,7 @@ structure ChildTrait (Self : Type) where
 /- [traits::test_child_trait1]: forward function
    Source: 'src/traits.rs', lines 209:0-209:56 -/
 def test_child_trait1
-  (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) :
-  Result alloc.string.String
-  :=
+  (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : Result String :=
   ChildTraitTInst.ParentTrait0SelfInst.get_name x
 
 /- [traits::test_child_trait2]: forward function
-- 
cgit v1.2.3


From 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 09:37:31 +0100
Subject: Update the generation of files for external definitions and
 regenerate the tests

---
 tests/coq/betree/BetreeMain_Funs.v                 |  4 +-
 tests/coq/betree/BetreeMain_FunsExternal.v         | 46 ++++++++++++++++++++++
 .../coq/betree/BetreeMain_FunsExternal_Template.v  | 46 ++++++++++++++++++++++
 tests/coq/betree/BetreeMain_Opaque.v               | 45 ---------------------
 tests/coq/betree/_CoqProject                       |  3 +-
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v       |  4 +-
 .../coq/hashmap_on_disk/HashmapMain_FunsExternal.v | 25 ++++++++++++
 .../HashmapMain_FunsExternal_Template.v            | 26 ++++++++++++
 tests/coq/hashmap_on_disk/HashmapMain_Opaque.v     | 25 ------------
 tests/coq/hashmap_on_disk/_CoqProject              |  3 +-
 tests/coq/misc/External_Funs.v                     |  4 +-
 tests/coq/misc/External_FunsExternal.v             | 43 ++++++++++++++++++++
 tests/coq/misc/External_FunsExternal_Template.v    | 44 +++++++++++++++++++++
 tests/coq/misc/External_Opaque.v                   | 43 --------------------
 tests/coq/misc/_CoqProject                         |  3 +-
 tests/fstar/betree/BetreeMain.Funs.fst             |  2 +-
 tests/fstar/betree/BetreeMain.FunsExternal.fsti    | 35 ++++++++++++++++
 tests/fstar/betree/BetreeMain.Opaque.fsti          | 35 ----------------
 .../fstar/betree_back_stateful/BetreeMain.Funs.fst |  2 +-
 .../BetreeMain.FunsExternal.fsti                   | 35 ++++++++++++++++
 .../betree_back_stateful/BetreeMain.Opaque.fsti    | 35 ----------------
 tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst   |  2 +-
 .../hashmap_on_disk/HashmapMain.FunsExternal.fsti  | 18 +++++++++
 .../fstar/hashmap_on_disk/HashmapMain.Opaque.fsti  | 18 ---------
 tests/fstar/misc/External.Funs.fst                 |  2 +-
 tests/fstar/misc/External.FunsExternal.fsti        | 32 +++++++++++++++
 tests/fstar/misc/External.Opaque.fsti              | 32 ---------------
 27 files changed, 366 insertions(+), 246 deletions(-)
 create mode 100644 tests/coq/betree/BetreeMain_FunsExternal.v
 create mode 100644 tests/coq/betree/BetreeMain_FunsExternal_Template.v
 delete mode 100644 tests/coq/betree/BetreeMain_Opaque.v
 create mode 100644 tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
 create mode 100644 tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
 delete mode 100644 tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
 create mode 100644 tests/coq/misc/External_FunsExternal.v
 create mode 100644 tests/coq/misc/External_FunsExternal_Template.v
 delete mode 100644 tests/coq/misc/External_Opaque.v
 create mode 100644 tests/fstar/betree/BetreeMain.FunsExternal.fsti
 delete mode 100644 tests/fstar/betree/BetreeMain.Opaque.fsti
 create mode 100644 tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
 delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
 create mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
 delete mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
 create mode 100644 tests/fstar/misc/External.FunsExternal.fsti
 delete mode 100644 tests/fstar/misc/External.Opaque.fsti

(limited to 'tests')

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 8e48b17d..ede82492 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -8,8 +8,8 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export BetreeMain_Types.
 Import BetreeMain_Types.
-Require Export BetreeMain_Opaque.
-Import BetreeMain_Opaque.
+Require Export BetreeMain_FunsExternal.
+Import BetreeMain_FunsExternal.
 Module BetreeMain_Funs.
 
 (** [betree_main::betree::load_internal_node]: forward function
diff --git a/tests/coq/betree/BetreeMain_FunsExternal.v b/tests/coq/betree/BetreeMain_FunsExternal.v
new file mode 100644
index 00000000..07dba263
--- /dev/null
+++ b/tests/coq/betree/BetreeMain_FunsExternal.v
@@ -0,0 +1,46 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export BetreeMain_Types.
+Import BetreeMain_Types.
+Module BetreeMain_FunsExternal.
+
+(** [betree_main::betree_utils::load_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
+Axiom betree_utils_load_internal_node
+  : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t)))
+.
+
+(** [betree_main::betree_utils::store_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
+Axiom betree_utils_store_internal_node
+  :
+  u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state *
+    unit)
+.
+
+(** [betree_main::betree_utils::load_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
+Axiom betree_utils_load_leaf_node
+  : u64 -> state -> result (state * (betree_List_t (u64 * u64)))
+.
+
+(** [betree_main::betree_utils::store_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
+Axiom betree_utils_store_leaf_node
+  : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
+.
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+Axiom core_option_Option_unwrap :
+  forall(T : Type), option T -> state -> result (state * T)
+.
+
+End BetreeMain_FunsExternal.
diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
new file mode 100644
index 00000000..4898acd4
--- /dev/null
+++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
@@ -0,0 +1,46 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export BetreeMain_Types.
+Import BetreeMain_Types.
+Module BetreeMain_FunsExternal_Template.
+
+(** [betree_main::betree_utils::load_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
+Axiom betree_utils_load_internal_node
+  : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t)))
+.
+
+(** [betree_main::betree_utils::store_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
+Axiom betree_utils_store_internal_node
+  :
+  u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state *
+    unit)
+.
+
+(** [betree_main::betree_utils::load_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
+Axiom betree_utils_load_leaf_node
+  : u64 -> state -> result (state * (betree_List_t (u64 * u64)))
+.
+
+(** [betree_main::betree_utils::store_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
+Axiom betree_utils_store_leaf_node
+  : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
+.
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+Axiom core_option_Option_unwrap :
+  forall(T : Type), option T -> state -> result (state * T)
+.
+
+End BetreeMain_FunsExternal_Template .
diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v
deleted file mode 100644
index a065c8a3..00000000
--- a/tests/coq/betree/BetreeMain_Opaque.v
+++ /dev/null
@@ -1,45 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external function declarations *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Require Import List.
-Import ListNotations.
-Local Open Scope Primitives_scope.
-Require Export BetreeMain_Types.
-Import BetreeMain_Types.
-Module BetreeMain_Opaque.
-
-(** [betree_main::betree_utils::load_internal_node]: forward function
-    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
-Axiom betree_utils_load_internal_node
-  : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t)))
-.
-
-(** [betree_main::betree_utils::store_internal_node]: forward function
-    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
-Axiom betree_utils_store_internal_node
-  :
-  u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state *
-    unit)
-.
-
-(** [betree_main::betree_utils::load_leaf_node]: forward function
-    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
-Axiom betree_utils_load_leaf_node
-  : u64 -> state -> result (state * (betree_List_t (u64 * u64)))
-.
-
-(** [betree_main::betree_utils::store_leaf_node]: forward function
-    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
-Axiom betree_utils_store_leaf_node
-  : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
-.
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-Axiom core_option_Option_unwrap :
-  forall(T : Type), option T -> state -> result (state * T)
-.
-
-End BetreeMain_Opaque .
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 42c62421..9ab8ea9f 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -5,5 +5,6 @@
 
 BetreeMain_Types.v
 Primitives.v
+BetreeMain_FunsExternal_Template.v
 BetreeMain_Funs.v
-BetreeMain_Opaque.v
+BetreeMain_FunsExternal.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 46d3ee29..188c98b3 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -8,8 +8,8 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export HashmapMain_Types.
 Import HashmapMain_Types.
-Require Export HashmapMain_Opaque.
-Import HashmapMain_Opaque.
+Require Export HashmapMain_FunsExternal.
+Import HashmapMain_FunsExternal.
 Module HashmapMain_Funs.
 
 (** [hashmap_main::hashmap::hash_key]: forward function
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
new file mode 100644
index 00000000..a03dc407
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
@@ -0,0 +1,25 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external function declarations *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export HashmapMain_Types.
+Import HashmapMain_Types.
+Module HashmapMain_FunsExternal.
+
+(** [hashmap_main::hashmap_utils::deserialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
+Axiom hashmap_utils_deserialize
+  : state -> result (state * (hashmap_HashMap_t u64))
+.
+
+(** [hashmap_main::hashmap_utils::serialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *)
+Axiom hashmap_utils_serialize
+  : hashmap_HashMap_t u64 -> state -> result (state * unit)
+.
+
+End HashmapMain_FunsExternal.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
new file mode 100644
index 00000000..b5a4a101
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
@@ -0,0 +1,26 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export HashmapMain_Types.
+Import HashmapMain_Types.
+Module HashmapMain_FunsExternal_Template.
+
+(** [hashmap_main::hashmap_utils::deserialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
+Axiom hashmap_utils_deserialize
+  : state -> result (state * (hashmap_HashMap_t u64))
+.
+
+(** [hashmap_main::hashmap_utils::serialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *)
+Axiom hashmap_utils_serialize
+  : hashmap_HashMap_t u64 -> state -> result (state * unit)
+.
+
+End HashmapMain_FunsExternal_Template .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
deleted file mode 100644
index a0e9003d..00000000
--- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
+++ /dev/null
@@ -1,25 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: external function declarations *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Require Import List.
-Import ListNotations.
-Local Open Scope Primitives_scope.
-Require Export HashmapMain_Types.
-Import HashmapMain_Types.
-Module HashmapMain_Opaque.
-
-(** [hashmap_main::hashmap_utils::deserialize]: forward function
-    Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
-Axiom hashmap_utils_deserialize
-  : state -> result (state * (hashmap_HashMap_t u64))
-.
-
-(** [hashmap_main::hashmap_utils::serialize]: forward function
-    Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *)
-Axiom hashmap_utils_serialize
-  : hashmap_HashMap_t u64 -> state -> result (state * unit)
-.
-
-End HashmapMain_Opaque .
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index b78c7b5f..a85fa1fe 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -6,4 +6,5 @@
 HashmapMain_Types.v
 Primitives.v
 HashmapMain_Funs.v
-HashmapMain_Opaque.v
+HashmapMain_FunsExternal_Template.v
+HashmapMain_FunsExternal.v
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 0a14c7d1..8a3360bb 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -8,8 +8,8 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export External_Types.
 Import External_Types.
-Require Export External_Opaque.
-Import External_Opaque.
+Require Export External_FunsExternal.
+Import External_FunsExternal.
 Module External_Funs.
 
 (** [external::swap]: forward function
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
new file mode 100644
index 00000000..07d43061
--- /dev/null
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -0,0 +1,43 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external function declarations *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export External_Types.
+Import External_Types.
+Module External_FunsExternal.
+
+(** [core::mem::swap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap :
+  forall(T : Type), T -> T -> state -> result (state * unit)
+.
+
+(** [core::mem::swap]: backward function 0
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap_back0 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::mem::swap]: backward function 1
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap_back1 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+Axiom core_num_nonzero_NonZeroU32_new
+  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
+.
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+Axiom core_option_Option_unwrap :
+  forall(T : Type), option T -> state -> result (state * T)
+.
+
+End External_FunsExternal.
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
new file mode 100644
index 00000000..0977c3ae
--- /dev/null
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -0,0 +1,44 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export External_Types.
+Import External_Types.
+Module External_FunsExternal_Template.
+
+(** [core::mem::swap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap :
+  forall(T : Type), T -> T -> state -> result (state * unit)
+.
+
+(** [core::mem::swap]: backward function 0
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap_back0 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::mem::swap]: backward function 1
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap_back1 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+Axiom core_num_nonzero_NonZeroU32_new
+  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
+.
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+Axiom core_option_Option_unwrap :
+  forall(T : Type), option T -> state -> result (state * T)
+.
+
+End External_FunsExternal_Template .
diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v
deleted file mode 100644
index b482431f..00000000
--- a/tests/coq/misc/External_Opaque.v
+++ /dev/null
@@ -1,43 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: external function declarations *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Require Import List.
-Import ListNotations.
-Local Open Scope Primitives_scope.
-Require Export External_Types.
-Import External_Types.
-Module External_Opaque.
-
-(** [core::mem::swap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Axiom core_mem_swap :
-  forall(T : Type), T -> T -> state -> result (state * unit)
-.
-
-(** [core::mem::swap]: backward function 0
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Axiom core_mem_swap_back0 :
-  forall(T : Type), T -> T -> state -> state -> result (state * T)
-.
-
-(** [core::mem::swap]: backward function 1
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Axiom core_mem_swap_back1 :
-  forall(T : Type), T -> T -> state -> state -> result (state * T)
-.
-
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
-Axiom core_num_nonzero_NonZeroU32_new
-  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
-.
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-Axiom core_option_Option_unwrap :
-  forall(T : Type), option T -> state -> result (state * T)
-.
-
-End External_Opaque .
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index db6c2742..6884d5d9 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -10,5 +10,6 @@ Constants.v
 PoloniusList.v
 External_Types.v
 NoNestedBorrows.v
-External_Opaque.v
+External_FunsExternal.v
+External_FunsExternal_Template.v
 Paper.v
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 537ec32e..fef8a8e1 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -3,7 +3,7 @@
 module BetreeMain.Funs
 open Primitives
 include BetreeMain.Types
-include BetreeMain.Opaque
+include BetreeMain.FunsExternal
 include BetreeMain.Clauses
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
new file mode 100644
index 00000000..cd2f956f
--- /dev/null
+++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
@@ -0,0 +1,35 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external function declarations *)
+module BetreeMain.FunsExternal
+open Primitives
+include BetreeMain.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree_utils::load_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
+val betree_utils_load_internal_node
+  : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
+
+(** [betree_main::betree_utils::store_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
+val betree_utils_store_internal_node
+  :
+  u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
+    unit)
+
+(** [betree_main::betree_utils::load_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
+val betree_utils_load_leaf_node
+  : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
+
+(** [betree_main::betree_utils::store_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
+val betree_utils_store_leaf_node
+  : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+val core_option_Option_unwrap
+  (t : Type0) : option t -> state -> result (state & t)
+
diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.Opaque.fsti
deleted file mode 100644
index b89c8718..00000000
--- a/tests/fstar/betree/BetreeMain.Opaque.fsti
+++ /dev/null
@@ -1,35 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external function declarations *)
-module BetreeMain.Opaque
-open Primitives
-include BetreeMain.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree_utils::load_internal_node]: forward function
-    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
-val betree_utils_load_internal_node
-  : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
-
-(** [betree_main::betree_utils::store_internal_node]: forward function
-    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
-val betree_utils_store_internal_node
-  :
-  u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
-    unit)
-
-(** [betree_main::betree_utils::load_leaf_node]: forward function
-    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
-val betree_utils_load_leaf_node
-  : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
-
-(** [betree_main::betree_utils::store_leaf_node]: forward function
-    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
-val betree_utils_store_leaf_node
-  : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-val core_option_Option_unwrap
-  (t : Type0) : option t -> state -> result (state & t)
-
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index a2586431..b912a316 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -3,7 +3,7 @@
 module BetreeMain.Funs
 open Primitives
 include BetreeMain.Types
-include BetreeMain.Opaque
+include BetreeMain.FunsExternal
 include BetreeMain.Clauses
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
new file mode 100644
index 00000000..cd2f956f
--- /dev/null
+++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
@@ -0,0 +1,35 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external function declarations *)
+module BetreeMain.FunsExternal
+open Primitives
+include BetreeMain.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree_utils::load_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
+val betree_utils_load_internal_node
+  : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
+
+(** [betree_main::betree_utils::store_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
+val betree_utils_store_internal_node
+  :
+  u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
+    unit)
+
+(** [betree_main::betree_utils::load_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
+val betree_utils_load_leaf_node
+  : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
+
+(** [betree_main::betree_utils::store_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
+val betree_utils_store_leaf_node
+  : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+val core_option_Option_unwrap
+  (t : Type0) : option t -> state -> result (state & t)
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
deleted file mode 100644
index b89c8718..00000000
--- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
+++ /dev/null
@@ -1,35 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external function declarations *)
-module BetreeMain.Opaque
-open Primitives
-include BetreeMain.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree_utils::load_internal_node]: forward function
-    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
-val betree_utils_load_internal_node
-  : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
-
-(** [betree_main::betree_utils::store_internal_node]: forward function
-    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
-val betree_utils_store_internal_node
-  :
-  u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
-    unit)
-
-(** [betree_main::betree_utils::load_leaf_node]: forward function
-    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
-val betree_utils_load_leaf_node
-  : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
-
-(** [betree_main::betree_utils::store_leaf_node]: forward function
-    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
-val betree_utils_store_leaf_node
-  : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-val core_option_Option_unwrap
-  (t : Type0) : option t -> state -> result (state & t)
-
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index fa570309..f2d09a38 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -3,7 +3,7 @@
 module HashmapMain.Funs
 open Primitives
 include HashmapMain.Types
-include HashmapMain.Opaque
+include HashmapMain.FunsExternal
 include HashmapMain.Clauses
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
new file mode 100644
index 00000000..b00bbcde
--- /dev/null
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
@@ -0,0 +1,18 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external function declarations *)
+module HashmapMain.FunsExternal
+open Primitives
+include HashmapMain.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [hashmap_main::hashmap_utils::deserialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
+val hashmap_utils_deserialize
+  : state -> result (state & (hashmap_HashMap_t u64))
+
+(** [hashmap_main::hashmap_utils::serialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *)
+val hashmap_utils_serialize
+  : hashmap_HashMap_t u64 -> state -> result (state & unit)
+
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
deleted file mode 100644
index 1f47eb33..00000000
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
+++ /dev/null
@@ -1,18 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: external function declarations *)
-module HashmapMain.Opaque
-open Primitives
-include HashmapMain.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [hashmap_main::hashmap_utils::deserialize]: forward function
-    Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
-val hashmap_utils_deserialize
-  : state -> result (state & (hashmap_HashMap_t u64))
-
-(** [hashmap_main::hashmap_utils::serialize]: forward function
-    Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *)
-val hashmap_utils_serialize
-  : hashmap_HashMap_t u64 -> state -> result (state & unit)
-
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 4d13fb71..00995634 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -3,7 +3,7 @@
 module External.Funs
 open Primitives
 include External.Types
-include External.Opaque
+include External.FunsExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
new file mode 100644
index 00000000..923a1101
--- /dev/null
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -0,0 +1,32 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external function declarations *)
+module External.FunsExternal
+open Primitives
+include External.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [core::mem::swap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+val core_mem_swap (t : Type0) : t -> t -> state -> result (state & unit)
+
+(** [core::mem::swap]: backward function 0
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+val core_mem_swap_back0
+  (t : Type0) : t -> t -> state -> state -> result (state & t)
+
+(** [core::mem::swap]: backward function 1
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+val core_mem_swap_back1
+  (t : Type0) : t -> t -> state -> state -> result (state & t)
+
+(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+val core_num_nonzero_NonZeroU32_new
+  : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+val core_option_Option_unwrap
+  (t : Type0) : option t -> state -> result (state & t)
+
diff --git a/tests/fstar/misc/External.Opaque.fsti b/tests/fstar/misc/External.Opaque.fsti
deleted file mode 100644
index ea1a70c2..00000000
--- a/tests/fstar/misc/External.Opaque.fsti
+++ /dev/null
@@ -1,32 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: external function declarations *)
-module External.Opaque
-open Primitives
-include External.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::mem::swap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-val core_mem_swap (t : Type0) : t -> t -> state -> result (state & unit)
-
-(** [core::mem::swap]: backward function 0
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-val core_mem_swap_back0
-  (t : Type0) : t -> t -> state -> state -> result (state & t)
-
-(** [core::mem::swap]: backward function 1
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-val core_mem_swap_back1
-  (t : Type0) : t -> t -> state -> state -> result (state & t)
-
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
-val core_num_nonzero_NonZeroU32_new
-  : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-val core_option_Option_unwrap
-  (t : Type0) : option t -> state -> result (state & t)
-
-- 
cgit v1.2.3


From bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 10:29:25 +0100
Subject: Generate a dedicated file for the external types

---
 tests/coq/array/Array.v                            |  2 +-
 tests/coq/betree/BetreeMain_Funs.v                 | 10 ++--
 .../coq/betree/BetreeMain_FunsExternal_Template.v  |  6 +--
 tests/coq/betree/BetreeMain_Types.v                |  7 ++-
 tests/coq/betree/BetreeMain_TypesExternal.v        | 15 ++++++
 .../coq/betree/BetreeMain_TypesExternal_Template.v | 15 ++++++
 tests/coq/betree/_CoqProject                       |  2 +
 tests/coq/hashmap/Hashmap_Funs.v                   |  6 +--
 tests/coq/hashmap/Hashmap_Types.v                  |  2 +-
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v       | 10 ++--
 .../HashmapMain_FunsExternal_Template.v            |  6 +--
 tests/coq/hashmap_on_disk/HashmapMain_Types.v      |  7 ++-
 .../hashmap_on_disk/HashmapMain_TypesExternal.v    | 15 ++++++
 .../HashmapMain_TypesExternal_Template.v           | 15 ++++++
 tests/coq/hashmap_on_disk/_CoqProject              |  2 +
 tests/coq/misc/Constants.v                         |  2 +-
 tests/coq/misc/External_Funs.v                     | 10 ++--
 tests/coq/misc/External_FunsExternal.v             |  2 +-
 tests/coq/misc/External_FunsExternal_Template.v    |  6 +--
 tests/coq/misc/External_Types.v                    | 11 ++--
 tests/coq/misc/External_TypesExternal.v            | 19 +++++++
 tests/coq/misc/External_TypesExternal_Template.v   | 19 +++++++
 tests/coq/misc/Loops.v                             |  2 +-
 tests/coq/misc/NoNestedBorrows.v                   |  2 +-
 tests/coq/misc/Paper.v                             |  2 +-
 tests/coq/misc/PoloniusList.v                      |  2 +-
 tests/coq/misc/_CoqProject                         |  6 ++-
 tests/coq/traits/Traits.v                          |  2 +-
 tests/fstar/betree/BetreeMain.Types.fst            | 61 +++++++++++++++++++++
 tests/fstar/betree/BetreeMain.Types.fsti           | 63 ----------------------
 tests/fstar/betree/BetreeMain.TypesExternal.fsti   | 10 ++++
 .../betree_back_stateful/BetreeMain.Types.fst      | 61 +++++++++++++++++++++
 .../betree_back_stateful/BetreeMain.Types.fsti     | 63 ----------------------
 .../BetreeMain.TypesExternal.fsti                  | 10 ++++
 tests/fstar/hashmap_on_disk/HashmapMain.Types.fst  | 24 +++++++++
 tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti | 26 ---------
 .../hashmap_on_disk/HashmapMain.TypesExternal.fsti | 10 ++++
 tests/fstar/misc/External.Types.fst                |  8 +++
 tests/fstar/misc/External.Types.fsti               | 14 -----
 tests/fstar/misc/External.TypesExternal.fsti       | 14 +++++
 tests/lean/BetreeMain/Types.lean                   |  4 +-
 tests/lean/BetreeMain/TypesExternal.lean           |  7 +++
 tests/lean/BetreeMain/TypesExternal_Template.lean  |  9 ++++
 tests/lean/External/Types.lean                     |  8 +--
 tests/lean/External/TypesExternal.lean             | 11 ++++
 tests/lean/External/TypesExternal_Template.lean    | 13 +++++
 tests/lean/HashmapMain/Types.lean                  |  4 +-
 tests/lean/HashmapMain/TypesExternal.lean          |  7 +++
 tests/lean/HashmapMain/TypesExternal_Template.lean |  9 ++++
 49 files changed, 408 insertions(+), 233 deletions(-)
 create mode 100644 tests/coq/betree/BetreeMain_TypesExternal.v
 create mode 100644 tests/coq/betree/BetreeMain_TypesExternal_Template.v
 create mode 100644 tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v
 create mode 100644 tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v
 create mode 100644 tests/coq/misc/External_TypesExternal.v
 create mode 100644 tests/coq/misc/External_TypesExternal_Template.v
 create mode 100644 tests/fstar/betree/BetreeMain.Types.fst
 delete mode 100644 tests/fstar/betree/BetreeMain.Types.fsti
 create mode 100644 tests/fstar/betree/BetreeMain.TypesExternal.fsti
 create mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Types.fst
 delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
 create mode 100644 tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti
 create mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
 delete mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
 create mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
 create mode 100644 tests/fstar/misc/External.Types.fst
 delete mode 100644 tests/fstar/misc/External.Types.fsti
 create mode 100644 tests/fstar/misc/External.TypesExternal.fsti
 create mode 100644 tests/lean/BetreeMain/TypesExternal.lean
 create mode 100644 tests/lean/BetreeMain/TypesExternal_Template.lean
 create mode 100644 tests/lean/External/TypesExternal.lean
 create mode 100644 tests/lean/External/TypesExternal_Template.lean
 create mode 100644 tests/lean/HashmapMain/TypesExternal.lean
 create mode 100644 tests/lean/HashmapMain/TypesExternal_Template.lean

(limited to 'tests')

diff --git a/tests/coq/array/Array.v b/tests/coq/array/Array.v
index 99ff3b03..105ce21f 100644
--- a/tests/coq/array/Array.v
+++ b/tests/coq/array/Array.v
@@ -528,4 +528,4 @@ Definition ite : result unit :=
   Return tt
 .
 
-End Array .
+End Array.
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index ede82492..aadaa20d 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export BetreeMain_Types.
-Import BetreeMain_Types.
-Require Export BetreeMain_FunsExternal.
-Import BetreeMain_FunsExternal.
+Require Import BetreeMain_Types.
+Include BetreeMain_Types.
+Require Import BetreeMain_FunsExternal.
+Include BetreeMain_FunsExternal.
 Module BetreeMain_Funs.
 
 (** [betree_main::betree::load_internal_node]: forward function
@@ -1230,4 +1230,4 @@ Definition main : result unit :=
 (** Unit test for [betree_main::main] *)
 Check (main )%return.
 
-End BetreeMain_Funs .
+End BetreeMain_Funs.
diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
index 4898acd4..36022a20 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v
+++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
@@ -7,8 +7,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export BetreeMain_Types.
-Import BetreeMain_Types.
+Require Import BetreeMain_Types.
+Include BetreeMain_Types.
 Module BetreeMain_FunsExternal_Template.
 
 (** [betree_main::betree_utils::load_internal_node]: forward function
@@ -43,4 +43,4 @@ Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
 
-End BetreeMain_FunsExternal_Template .
+End BetreeMain_FunsExternal_Template.
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index b729d1c3..22989256 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -6,6 +6,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
+Require Import BetreeMain_TypesExternal.
+Include BetreeMain_TypesExternal.
 Module BetreeMain_Types.
 
 (** [betree_main::betree::List]
@@ -113,7 +115,4 @@ mkbetree_BeTree_t {
 }
 .
 
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End BetreeMain_Types .
+End BetreeMain_Types.
diff --git a/tests/coq/betree/BetreeMain_TypesExternal.v b/tests/coq/betree/BetreeMain_TypesExternal.v
new file mode 100644
index 00000000..50c4a4f8
--- /dev/null
+++ b/tests/coq/betree/BetreeMain_TypesExternal.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module BetreeMain_TypesExternal.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End BetreeMain_TypesExternal.
diff --git a/tests/coq/betree/BetreeMain_TypesExternal_Template.v b/tests/coq/betree/BetreeMain_TypesExternal_Template.v
new file mode 100644
index 00000000..651de2b7
--- /dev/null
+++ b/tests/coq/betree/BetreeMain_TypesExternal_Template.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module BetreeMain_TypesExternal_Template.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End BetreeMain_TypesExternal_Template.
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 9ab8ea9f..13e4b9c1 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -4,7 +4,9 @@
 -arg all
 
 BetreeMain_Types.v
+BetreeMain_TypesExternal_Template.v
 Primitives.v
 BetreeMain_FunsExternal_Template.v
 BetreeMain_Funs.v
+BetreeMain_TypesExternal.v
 BetreeMain_FunsExternal.v
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index c08f7f7d..64de44a6 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -6,8 +6,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export Hashmap_Types.
-Import Hashmap_Types.
+Require Import Hashmap_Types.
+Include Hashmap_Types.
 Module Hashmap_Funs.
 
 (** [hashmap::hash_key]: forward function
@@ -668,4 +668,4 @@ Definition test1 (n : nat) : result unit :=
       end))
 .
 
-End Hashmap_Funs .
+End Hashmap_Funs.
diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v
index bfb5ae4b..80a43593 100644
--- a/tests/coq/hashmap/Hashmap_Types.v
+++ b/tests/coq/hashmap/Hashmap_Types.v
@@ -35,4 +35,4 @@ Arguments hashMap_max_load_factor { _ }.
 Arguments hashMap_max_load { _ }.
 Arguments hashMap_slots { _ }.
 
-End Hashmap_Types .
+End Hashmap_Types.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 188c98b3..faba0afe 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export HashmapMain_Types.
-Import HashmapMain_Types.
-Require Export HashmapMain_FunsExternal.
-Import HashmapMain_FunsExternal.
+Require Import HashmapMain_Types.
+Include HashmapMain_Types.
+Require Import HashmapMain_FunsExternal.
+Include HashmapMain_FunsExternal.
 Module HashmapMain_Funs.
 
 (** [hashmap_main::hashmap::hash_key]: forward function
@@ -717,4 +717,4 @@ Definition insert_on_disk
 Definition main : result unit :=
   Return tt.
 
-End HashmapMain_Funs .
+End HashmapMain_Funs.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
index b5a4a101..e10d02f6 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
@@ -7,8 +7,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export HashmapMain_Types.
-Import HashmapMain_Types.
+Require Import HashmapMain_Types.
+Include HashmapMain_Types.
 Module HashmapMain_FunsExternal_Template.
 
 (** [hashmap_main::hashmap_utils::deserialize]: forward function
@@ -23,4 +23,4 @@ Axiom hashmap_utils_serialize
   : hashmap_HashMap_t u64 -> state -> result (state * unit)
 .
 
-End HashmapMain_FunsExternal_Template .
+End HashmapMain_FunsExternal_Template.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
index 039b7e72..8d3d72aa 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
@@ -6,6 +6,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
+Require Import HashmapMain_TypesExternal.
+Include HashmapMain_TypesExternal.
 Module HashmapMain_Types.
 
 (** [hashmap_main::hashmap::List]
@@ -35,7 +37,4 @@ Arguments hashmap_HashMap_max_load_factor { _ }.
 Arguments hashmap_HashMap_max_load { _ }.
 Arguments hashmap_HashMap_slots { _ }.
 
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End HashmapMain_Types .
+End HashmapMain_Types.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v
new file mode 100644
index 00000000..87568232
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module HashmapMain_TypesExternal.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End HashmapMain_TypesExternal.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v
new file mode 100644
index 00000000..391b2775
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module HashmapMain_TypesExternal_Template.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End HashmapMain_TypesExternal_Template.
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index a85fa1fe..41945494 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -6,5 +6,7 @@
 HashmapMain_Types.v
 Primitives.v
 HashmapMain_Funs.v
+HashmapMain_TypesExternal.v
 HashmapMain_FunsExternal_Template.v
 HashmapMain_FunsExternal.v
+HashmapMain_TypesExternal_Template.v
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 20edb2b1..ad899f25 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -157,4 +157,4 @@ Definition s3_c : Pair_t u32 u32 := s3_body%global.
 Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32.
 Definition s4_c : Pair_t u32 u32 := s4_body%global.
 
-End Constants .
+End Constants.
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 8a3360bb..e9d39f66 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export External_Types.
-Import External_Types.
-Require Export External_FunsExternal.
-Import External_FunsExternal.
+Require Import External_Types.
+Include External_Types.
+Require Import External_FunsExternal.
+Include External_FunsExternal.
 Module External_Funs.
 
 (** [external::swap]: forward function
@@ -115,4 +115,4 @@ Definition test_swap_non_zero (x : u32) (st : state) : result (state * u32) :=
   if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0)
 .
 
-End External_Funs .
+End External_Funs.
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
index 07d43061..a8c5756a 100644
--- a/tests/coq/misc/External_FunsExternal.v
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -7,7 +7,7 @@ Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export External_Types.
-Import External_Types.
+Include External_Types.
 Module External_FunsExternal.
 
 (** [core::mem::swap]: forward function
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 0977c3ae..31e69c39 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -7,8 +7,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export External_Types.
-Import External_Types.
+Require Import External_Types.
+Include External_Types.
 Module External_FunsExternal_Template.
 
 (** [core::mem::swap]: forward function
@@ -41,4 +41,4 @@ Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
 
-End External_FunsExternal_Template .
+End External_FunsExternal_Template.
diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v
index c638670c..b42c2ecf 100644
--- a/tests/coq/misc/External_Types.v
+++ b/tests/coq/misc/External_Types.v
@@ -6,13 +6,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
+Require Import External_TypesExternal.
+Include External_TypesExternal.
 Module External_Types.
 
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
-Axiom core_num_nonzero_NonZeroU32_t : Type.
-
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End External_Types .
+End External_Types.
diff --git a/tests/coq/misc/External_TypesExternal.v b/tests/coq/misc/External_TypesExternal.v
new file mode 100644
index 00000000..3f02b839
--- /dev/null
+++ b/tests/coq/misc/External_TypesExternal.v
@@ -0,0 +1,19 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module External_TypesExternal.
+
+(** [core::num::nonzero::NonZeroU32]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+Axiom core_num_nonzero_NonZeroU32_t : Type.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End External_TypesExternal.
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
new file mode 100644
index 00000000..7ba79d8e
--- /dev/null
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -0,0 +1,19 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module External_TypesExternal_Template.
+
+(** [core::num::nonzero::NonZeroU32]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+Axiom core_num_nonzero_NonZeroU32_t : Type.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End External_TypesExternal_Template.
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 4929ddd0..83c249c1 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -914,4 +914,4 @@ Definition list_nth_shared_mut_loop_pair_merge_back
   list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
 .
 
-End Loops .
+End Loops.
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index b044d24f..16a2e816 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -586,4 +586,4 @@ Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 :=
 Definition test_shared_borrow_enum2 : result u32 :=
   Return 0%u32.
 
-End NoNestedBorrows .
+End NoNestedBorrows.
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 4a49096f..6b110193 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -128,4 +128,4 @@ Definition call_choose (p : (u32 * u32)) : result u32 :=
   Return px0
 .
 
-End Paper .
+End Paper.
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index a0820e40..2371b1cc 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -41,4 +41,4 @@ Fixpoint get_list_at_x_back
   end
 .
 
-End PoloniusList .
+End PoloniusList.
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 6884d5d9..0828bced 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -4,12 +4,14 @@
 -arg all
 
 Loops.v
+External_Types.v
 Primitives.v
 External_Funs.v
+Paper.v
+External_TypesExternal.v
 Constants.v
 PoloniusList.v
-External_Types.v
 NoNestedBorrows.v
 External_FunsExternal.v
+External_TypesExternal_Template.v
 External_FunsExternal_Template.v
-Paper.v
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 50eaf848..ebdca4ec 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -611,4 +611,4 @@ Arguments CFn_t_call_mut { _ _ }.
 Definition incr_u32 (x : u32) : result u32 :=
   u32_add x 1%u32.
 
-End Traits .
+End Traits.
diff --git a/tests/fstar/betree/BetreeMain.Types.fst b/tests/fstar/betree/BetreeMain.Types.fst
new file mode 100644
index 00000000..b87219b2
--- /dev/null
+++ b/tests/fstar/betree/BetreeMain.Types.fst
@@ -0,0 +1,61 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: type definitions *)
+module BetreeMain.Types
+open Primitives
+include BetreeMain.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree::List]
+    Source: 'src/betree.rs', lines 17:0-17:23 *)
+type betree_List_t (t : Type0) =
+| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
+| Betree_List_Nil : betree_List_t t
+
+(** [betree_main::betree::UpsertFunState]
+    Source: 'src/betree.rs', lines 63:0-63:23 *)
+type betree_UpsertFunState_t =
+| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
+| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
+
+(** [betree_main::betree::Message]
+    Source: 'src/betree.rs', lines 69:0-69:23 *)
+type betree_Message_t =
+| Betree_Message_Insert : u64 -> betree_Message_t
+| Betree_Message_Delete : betree_Message_t
+| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
+
+(** [betree_main::betree::Leaf]
+    Source: 'src/betree.rs', lines 167:0-167:11 *)
+type betree_Leaf_t = { id : u64; size : u64; }
+
+(** [betree_main::betree::Internal]
+    Source: 'src/betree.rs', lines 156:0-156:15 *)
+type betree_Internal_t =
+{
+  id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
+}
+
+(** [betree_main::betree::Node]
+    Source: 'src/betree.rs', lines 179:0-179:9 *)
+and betree_Node_t =
+| Betree_Node_Internal : betree_Internal_t -> betree_Node_t
+| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
+
+(** [betree_main::betree::Params]
+    Source: 'src/betree.rs', lines 187:0-187:13 *)
+type betree_Params_t = { min_flush_size : u64; split_size : u64; }
+
+(** [betree_main::betree::NodeIdCounter]
+    Source: 'src/betree.rs', lines 201:0-201:20 *)
+type betree_NodeIdCounter_t = { next_node_id : u64; }
+
+(** [betree_main::betree::BeTree]
+    Source: 'src/betree.rs', lines 218:0-218:17 *)
+type betree_BeTree_t =
+{
+  params : betree_Params_t;
+  node_id_cnt : betree_NodeIdCounter_t;
+  root : betree_Node_t;
+}
+
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti
deleted file mode 100644
index a098ec19..00000000
--- a/tests/fstar/betree/BetreeMain.Types.fsti
+++ /dev/null
@@ -1,63 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: type definitions *)
-module BetreeMain.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree::List]
-    Source: 'src/betree.rs', lines 17:0-17:23 *)
-type betree_List_t (t : Type0) =
-| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
-| Betree_List_Nil : betree_List_t t
-
-(** [betree_main::betree::UpsertFunState]
-    Source: 'src/betree.rs', lines 63:0-63:23 *)
-type betree_UpsertFunState_t =
-| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
-| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
-
-(** [betree_main::betree::Message]
-    Source: 'src/betree.rs', lines 69:0-69:23 *)
-type betree_Message_t =
-| Betree_Message_Insert : u64 -> betree_Message_t
-| Betree_Message_Delete : betree_Message_t
-| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
-
-(** [betree_main::betree::Leaf]
-    Source: 'src/betree.rs', lines 167:0-167:11 *)
-type betree_Leaf_t = { id : u64; size : u64; }
-
-(** [betree_main::betree::Internal]
-    Source: 'src/betree.rs', lines 156:0-156:15 *)
-type betree_Internal_t =
-{
-  id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
-}
-
-(** [betree_main::betree::Node]
-    Source: 'src/betree.rs', lines 179:0-179:9 *)
-and betree_Node_t =
-| Betree_Node_Internal : betree_Internal_t -> betree_Node_t
-| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
-
-(** [betree_main::betree::Params]
-    Source: 'src/betree.rs', lines 187:0-187:13 *)
-type betree_Params_t = { min_flush_size : u64; split_size : u64; }
-
-(** [betree_main::betree::NodeIdCounter]
-    Source: 'src/betree.rs', lines 201:0-201:20 *)
-type betree_NodeIdCounter_t = { next_node_id : u64; }
-
-(** [betree_main::betree::BeTree]
-    Source: 'src/betree.rs', lines 218:0-218:17 *)
-type betree_BeTree_t =
-{
-  params : betree_Params_t;
-  node_id_cnt : betree_NodeIdCounter_t;
-  root : betree_Node_t;
-}
-
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/betree/BetreeMain.TypesExternal.fsti b/tests/fstar/betree/BetreeMain.TypesExternal.fsti
new file mode 100644
index 00000000..1b2c53a6
--- /dev/null
+++ b/tests/fstar/betree/BetreeMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external type declarations *)
+module BetreeMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fst b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
new file mode 100644
index 00000000..b87219b2
--- /dev/null
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
@@ -0,0 +1,61 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: type definitions *)
+module BetreeMain.Types
+open Primitives
+include BetreeMain.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree::List]
+    Source: 'src/betree.rs', lines 17:0-17:23 *)
+type betree_List_t (t : Type0) =
+| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
+| Betree_List_Nil : betree_List_t t
+
+(** [betree_main::betree::UpsertFunState]
+    Source: 'src/betree.rs', lines 63:0-63:23 *)
+type betree_UpsertFunState_t =
+| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
+| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
+
+(** [betree_main::betree::Message]
+    Source: 'src/betree.rs', lines 69:0-69:23 *)
+type betree_Message_t =
+| Betree_Message_Insert : u64 -> betree_Message_t
+| Betree_Message_Delete : betree_Message_t
+| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
+
+(** [betree_main::betree::Leaf]
+    Source: 'src/betree.rs', lines 167:0-167:11 *)
+type betree_Leaf_t = { id : u64; size : u64; }
+
+(** [betree_main::betree::Internal]
+    Source: 'src/betree.rs', lines 156:0-156:15 *)
+type betree_Internal_t =
+{
+  id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
+}
+
+(** [betree_main::betree::Node]
+    Source: 'src/betree.rs', lines 179:0-179:9 *)
+and betree_Node_t =
+| Betree_Node_Internal : betree_Internal_t -> betree_Node_t
+| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
+
+(** [betree_main::betree::Params]
+    Source: 'src/betree.rs', lines 187:0-187:13 *)
+type betree_Params_t = { min_flush_size : u64; split_size : u64; }
+
+(** [betree_main::betree::NodeIdCounter]
+    Source: 'src/betree.rs', lines 201:0-201:20 *)
+type betree_NodeIdCounter_t = { next_node_id : u64; }
+
+(** [betree_main::betree::BeTree]
+    Source: 'src/betree.rs', lines 218:0-218:17 *)
+type betree_BeTree_t =
+{
+  params : betree_Params_t;
+  node_id_cnt : betree_NodeIdCounter_t;
+  root : betree_Node_t;
+}
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
deleted file mode 100644
index a098ec19..00000000
--- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
+++ /dev/null
@@ -1,63 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: type definitions *)
-module BetreeMain.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree::List]
-    Source: 'src/betree.rs', lines 17:0-17:23 *)
-type betree_List_t (t : Type0) =
-| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
-| Betree_List_Nil : betree_List_t t
-
-(** [betree_main::betree::UpsertFunState]
-    Source: 'src/betree.rs', lines 63:0-63:23 *)
-type betree_UpsertFunState_t =
-| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
-| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
-
-(** [betree_main::betree::Message]
-    Source: 'src/betree.rs', lines 69:0-69:23 *)
-type betree_Message_t =
-| Betree_Message_Insert : u64 -> betree_Message_t
-| Betree_Message_Delete : betree_Message_t
-| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
-
-(** [betree_main::betree::Leaf]
-    Source: 'src/betree.rs', lines 167:0-167:11 *)
-type betree_Leaf_t = { id : u64; size : u64; }
-
-(** [betree_main::betree::Internal]
-    Source: 'src/betree.rs', lines 156:0-156:15 *)
-type betree_Internal_t =
-{
-  id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
-}
-
-(** [betree_main::betree::Node]
-    Source: 'src/betree.rs', lines 179:0-179:9 *)
-and betree_Node_t =
-| Betree_Node_Internal : betree_Internal_t -> betree_Node_t
-| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
-
-(** [betree_main::betree::Params]
-    Source: 'src/betree.rs', lines 187:0-187:13 *)
-type betree_Params_t = { min_flush_size : u64; split_size : u64; }
-
-(** [betree_main::betree::NodeIdCounter]
-    Source: 'src/betree.rs', lines 201:0-201:20 *)
-type betree_NodeIdCounter_t = { next_node_id : u64; }
-
-(** [betree_main::betree::BeTree]
-    Source: 'src/betree.rs', lines 218:0-218:17 *)
-type betree_BeTree_t =
-{
-  params : betree_Params_t;
-  node_id_cnt : betree_NodeIdCounter_t;
-  root : betree_Node_t;
-}
-
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti
new file mode 100644
index 00000000..1b2c53a6
--- /dev/null
+++ b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external type declarations *)
+module BetreeMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
new file mode 100644
index 00000000..afebcde3
--- /dev/null
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: type definitions *)
+module HashmapMain.Types
+open Primitives
+include HashmapMain.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [hashmap_main::hashmap::List]
+    Source: 'src/hashmap.rs', lines 19:0-19:16 *)
+type hashmap_List_t (t : Type0) =
+| Hashmap_List_Cons : usize -> t -> hashmap_List_t t -> hashmap_List_t t
+| Hashmap_List_Nil : hashmap_List_t t
+
+(** [hashmap_main::hashmap::HashMap]
+    Source: 'src/hashmap.rs', lines 35:0-35:21 *)
+type hashmap_HashMap_t (t : Type0) =
+{
+  num_entries : usize;
+  max_load_factor : (usize & usize);
+  max_load : usize;
+  slots : alloc_vec_Vec (hashmap_List_t t);
+}
+
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
deleted file mode 100644
index e77954ad..00000000
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
+++ /dev/null
@@ -1,26 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: type definitions *)
-module HashmapMain.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [hashmap_main::hashmap::List]
-    Source: 'src/hashmap.rs', lines 19:0-19:16 *)
-type hashmap_List_t (t : Type0) =
-| Hashmap_List_Cons : usize -> t -> hashmap_List_t t -> hashmap_List_t t
-| Hashmap_List_Nil : hashmap_List_t t
-
-(** [hashmap_main::hashmap::HashMap]
-    Source: 'src/hashmap.rs', lines 35:0-35:21 *)
-type hashmap_HashMap_t (t : Type0) =
-{
-  num_entries : usize;
-  max_load_factor : (usize & usize);
-  max_load : usize;
-  slots : alloc_vec_Vec (hashmap_List_t t);
-}
-
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
new file mode 100644
index 00000000..75747408
--- /dev/null
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external type declarations *)
+module HashmapMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst
new file mode 100644
index 00000000..4fbcec47
--- /dev/null
+++ b/tests/fstar/misc/External.Types.fst
@@ -0,0 +1,8 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: type definitions *)
+module External.Types
+open Primitives
+include External.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
diff --git a/tests/fstar/misc/External.Types.fsti b/tests/fstar/misc/External.Types.fsti
deleted file mode 100644
index 0cb9fd0e..00000000
--- a/tests/fstar/misc/External.Types.fsti
+++ /dev/null
@@ -1,14 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: type definitions *)
-module External.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
-val core_num_nonzero_NonZeroU32_t : Type0
-
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
new file mode 100644
index 00000000..4bfbe0c5
--- /dev/null
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -0,0 +1,14 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external type declarations *)
+module External.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [core::num::nonzero::NonZeroU32]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+val core_num_nonzero_NonZeroU32_t : Type0
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 6e528437..877508f6 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -1,6 +1,7 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [betree_main]: type definitions
 import Base
+import BetreeMain.TypesExternal
 open Primitives
 
 namespace betree_main
@@ -63,7 +64,4 @@ structure betree.BeTree where
   node_id_cnt : betree.NodeIdCounter
   root : betree.Node
 
-/- The state type used in the state-error monad -/
-axiom State : Type
-
 end betree_main
diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/BetreeMain/TypesExternal.lean
new file mode 100644
index 00000000..1701eaaf
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal.lean
@@ -0,0 +1,7 @@
+-- [betree_main]: external types.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/BetreeMain/TypesExternal_Template.lean
new file mode 100644
index 00000000..bbac7e99
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal_Template.lean
@@ -0,0 +1,9 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [betree_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 40f20cda..961f3e8a 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -1,15 +1,9 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [external]: type definitions
 import Base
+import External.TypesExternal
 open Primitives
 
 namespace external
 
-/- [core::num::nonzero::NonZeroU32]
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
-axiom core.num.nonzero.NonZeroU32 : Type
-
-/- The state type used in the state-error monad -/
-axiom State : Type
-
 end external
diff --git a/tests/lean/External/TypesExternal.lean b/tests/lean/External/TypesExternal.lean
new file mode 100644
index 00000000..7c30f792
--- /dev/null
+++ b/tests/lean/External/TypesExternal.lean
@@ -0,0 +1,11 @@
+-- [external]: external types.
+import Base
+open Primitives
+
+/- [core::num::nonzero::NonZeroU32]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+axiom core.num.nonzero.NonZeroU32 : Type
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
new file mode 100644
index 00000000..85fef236
--- /dev/null
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -0,0 +1,13 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [external]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- [core::num::nonzero::NonZeroU32]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+axiom core.num.nonzero.NonZeroU32 : Type
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
index f7be6719..ae9ac999 100644
--- a/tests/lean/HashmapMain/Types.lean
+++ b/tests/lean/HashmapMain/Types.lean
@@ -1,6 +1,7 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [hashmap_main]: type definitions
 import Base
+import HashmapMain.TypesExternal
 open Primitives
 
 namespace hashmap_main
@@ -19,7 +20,4 @@ structure hashmap.HashMap (T : Type) where
   max_load : Usize
   slots : alloc.vec.Vec (hashmap.List T)
 
-/- The state type used in the state-error monad -/
-axiom State : Type
-
 end hashmap_main
diff --git a/tests/lean/HashmapMain/TypesExternal.lean b/tests/lean/HashmapMain/TypesExternal.lean
new file mode 100644
index 00000000..4e1cdbe9
--- /dev/null
+++ b/tests/lean/HashmapMain/TypesExternal.lean
@@ -0,0 +1,7 @@
+-- [hashmap_main]: external types.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/HashmapMain/TypesExternal_Template.lean b/tests/lean/HashmapMain/TypesExternal_Template.lean
new file mode 100644
index 00000000..cfa8bbb1
--- /dev/null
+++ b/tests/lean/HashmapMain/TypesExternal_Template.lean
@@ -0,0 +1,9 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
-- 
cgit v1.2.3