Merge pull request #46 from AeneasVerif/son_improves

Minor improvements for the extraction

94 files changed, 917 insertions, 521 deletions

diff --git a/Makefile b/Makefile
index e0367d73..88cb7d05 100644
--- a/Makefile
+++ b/Makefile
@@ -30,11 +30,8 @@ CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
 AENEAS_EXE ?= bin/aeneas
 
 # The user can specify additional translation options for Aeneas.
-# By default we do:
-# - unfold all the monadic let bindings to matches (required by F*)
-# - insert calls to the normalizer in the translated code to test the
-#   generated unit functions
-OPTIONS +=
+# By default we activate the (expensive) sanity checks.
+OPTIONS ?= -checks
 
 #
 # The rules use (and update) the following variables
diff --git a/compiler/Config.ml b/compiler/Config.ml
index fe110ee4..364ef748 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -35,11 +35,11 @@ let backend = ref FStar
 
 (** {1 Interpreter} *)
 
-(** Check that invariants are maintained whenever we execute a statement
-
-    TODO: rename to sanity_checks.
+(** Activate the sanity checks, and in particular the invariant checks
+    that are performed at every evaluation step. This is very expensive
+    (~100x slow down) but very efficient to catch mistakes early.
  *)
-let check_invariants = ref true
+let sanity_checks = ref false
 
 (** Expand all symbolic values containing borrows upon introduction - allows
     to use restrict ourselves to a simpler model for the projectors over
@@ -52,7 +52,8 @@ let greedy_expand_symbolics_with_borrows = true
 
 (** Experimental.
 
-    TODO: remove (always true now)
+    TODO: remove (always true now), but check that when we panic/call a function
+    there is no bottom below a borrow.
 
     We sometimes want to temporarily break the invariant that there is no
     bottom value below a borrow. If this value is true, we don't check
@@ -288,7 +289,7 @@ let unfold_monadic_let_bindings = ref false
     we later filter the useless *forward* calls in the micro-passes, where it is
     more natural to do.
 
-    See the comments for {!val:PureMicroPasses.expression_contains_child_call_in_all_paths}
+    See the comments for {!PureMicroPasses.expression_contains_child_call_in_all_paths}
     for additional explanations.
  *)
 let filter_useless_monadic_calls = ref true
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index a2ae4f16..c93bb213 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -112,7 +112,7 @@ let reset_global_counters () =
   fun_call_id_counter := FunCallId.generator_zero;
   dummy_var_id_counter := DummyVarId.generator_zero
 
-(** Ancestor for {!env} iter visitor *)
+(** Ancestor for {!type:env} iter visitor *)
 class ['self] iter_env_base =
   object (_self : 'self)
     inherit [_] iter_abs
@@ -120,7 +120,7 @@ class ['self] iter_env_base =
     method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for {!env} map visitor *)
+(** Ancestor for {!type:env} map visitor *)
 class ['self] map_env_base =
   object (_self : 'self)
     inherit [_] map_abs
@@ -423,11 +423,11 @@ let erase_regions (ty : ty) : ty =
   in
   v#visit_ty () ty
 
-(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.Bottom}) *)
+(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
   ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))
 
-(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.Bottom}) *)
+(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
   let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
   ctx_push_vars ctx vars
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index c8c16c08..e48e6ae6 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -173,12 +173,7 @@ let extract_adt_g_value
          *)
         let cons =
           match variant_id with
-          | Some vid -> (
-              (* In the case of Lean, we might have to add the type name as a prefix *)
-              match (!backend, adt_id) with
-              | Lean, TAssumed _ ->
-                  ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx
-              | _ -> ctx_get_variant adt_id vid ctx)
+          | Some vid -> ctx_get_variant adt_id vid ctx
           | None -> ctx_get_struct adt_id ctx
         in
         let use_parentheses = inside && field_values <> [] in
@@ -2723,7 +2718,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt "==";
         F.pp_print_space fmt ();
         let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in
-        F.pp_print_string fmt ("." ^ success ^ " ())")
+        F.pp_print_string fmt (success ^ " ())")
     | HOL4 ->
         F.pp_print_string fmt "val _ = assert_return (";
         F.pp_print_string fmt "“";
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index c6158847..85ab1112 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -311,7 +311,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
     the same name because Lean uses the typing information to resolve the
     ambiguities.
 
-    This map complements the {!names_map}, which checks for collisions.
+    This map complements the {!type:names_map}, which checks for collisions.
   *)
 type unsafe_names_map = { id_to_name : string IdMap.t }
 
@@ -634,11 +634,13 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   | TypeId id -> "type name: " ^ type_id_to_string ctx id
   | StructId id -> "struct constructor of: " ^ type_id_to_string ctx id
   | VariantId (id, variant_id) ->
+      let type_name = type_id_to_string ctx id in
       let variant_name = adt_variant_to_string ctx id (Some variant_id) in
-      "variant name: " ^ variant_name
+      "type name: " ^ type_name ^ ", variant name: " ^ variant_name
   | FieldId (id, field_id) ->
+      let type_name = type_id_to_string ctx id in
       let field_name = adt_field_to_string ctx id field_id in
-      "field name: " ^ field_name
+      "type name: " ^ type_name ^ ", field name: " ^ field_name
   | UnknownId -> "keyword"
   | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id
   | ConstGenericVarId id ->
@@ -958,31 +960,40 @@ let keywords () =
   List.concat [ named_unops; named_binops; misc ]
 
 let assumed_adts () : (assumed_ty * string) list =
-  match !backend with
-  | Lean ->
-      [
-        (TState, "State");
-        (TResult, "Result");
-        (TError, "Error");
-        (TFuel, "Nat");
-        (TArray, "Array");
-        (TSlice, "Slice");
-        (TStr, "Str");
-        (TRawPtr Mut, "MutRawPtr");
-        (TRawPtr Const, "ConstRawPtr");
-      ]
-  | Coq | FStar | HOL4 ->
-      [
-        (TState, "state");
-        (TResult, "result");
-        (TError, "error");
-        (TFuel, if !backend = HOL4 then "num" else "nat");
-        (TArray, "array");
-        (TSlice, "slice");
-        (TStr, "str");
-        (TRawPtr Mut, "mut_raw_ptr");
-        (TRawPtr Const, "const_raw_ptr");
-      ]
+  let state =
+    if !use_state then
+      match !backend with
+      | Lean -> [ (TState, "State") ]
+      | Coq | FStar | HOL4 -> [ (TState, "state") ]
+    else []
+  in
+  (* We voluntarily omit the type [Error]: it is never directly
+     referenced in the generated translation, and easily collides
+     with user-defined types *)
+  let adts =
+    match !backend with
+    | Lean ->
+        [
+          (TResult, "Result");
+          (TFuel, "Nat");
+          (TArray, "Array");
+          (TSlice, "Slice");
+          (TStr, "Str");
+          (TRawPtr Mut, "MutRawPtr");
+          (TRawPtr Const, "ConstRawPtr");
+        ]
+    | Coq | FStar | HOL4 ->
+        [
+          (TResult, "result");
+          (TFuel, if !backend = HOL4 then "num" else "nat");
+          (TArray, "array");
+          (TSlice, "slice");
+          (TStr, "str");
+          (TRawPtr Mut, "mut_raw_ptr");
+          (TRawPtr Const, "const_raw_ptr");
+        ]
+  in
+  state @ adts
 
 let assumed_struct_constructors () : (assumed_ty * string) list =
   match !backend with
@@ -1013,9 +1024,12 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
       ]
   | Lean ->
       [
-        (TResult, result_return_id, "ret");
-        (TResult, result_fail_id, "fail");
-        (TError, error_failure_id, "panic");
+        (TResult, result_return_id, "Result.ret");
+        (TResult, result_fail_id, "Result.fail");
+        (* For panic: we omit the prefix "Error." because the type is always
+           clear from the context. Also, "Error" is often used by user-defined
+           types (when we omit the crate as a prefix). *)
+        (TError, error_failure_id, ".panic");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
       ]
@@ -1095,8 +1109,9 @@ let initialize_names_maps () : names_maps =
   let init = names_map_init () in
   let int_names = List.map int_name T.all_int_types in
   let keywords =
-    List.concat
-      [ [ bool_name (); char_name (); str_name () ]; int_names; init.keywords ]
+    (* Remark: we don't put "str_name()" below because it clashes with
+       "alloc::string::String", which we register elsewhere. *)
+    List.concat [ [ bool_name (); char_name () ]; int_names; init.keywords ]
   in
   let names_set = StringSet.empty in
   let name_to_id = StringMap.empty in
@@ -1405,9 +1420,10 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
        - we add "_fwd"
      - [rg] is [None]: this is a backward function:
        - this function has one extracted backward function:
-         - if the forward function has been filtered, we add "_fwd_back":
+         - if the forward function has been filtered, we add nothing:
            the forward function is useless, so the unique backward function
-           takes its place, in a way
+           takes its place, in a way (in effect, we "merge" the forward
+           and the backward functions).
          - otherwise we add "_back"
        - this function has several backward functions: we add "_back" and an
          additional suffix to identify the precise backward function
@@ -1623,7 +1639,7 @@ let ctx_compute_trait_type_clause_name (ctx : extraction_ctx)
       function is an assumed function or a local function
     - function basename
     - the number of loops in the parent function. This is used for
-      the same purpose as in {!field:llbc_name}.
+      the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
 let ctx_compute_termination_measure_name (ctx : extraction_ctx)
@@ -1652,7 +1668,7 @@ let ctx_compute_termination_measure_name (ctx : extraction_ctx)
       function is an assumed function or a local function
     - function basename
     - the number of loops in the parent function. This is used for
-      the same purpose as in {!field:llbc_name}.
+      the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
 let ctx_compute_decreases_proof_name (ctx : extraction_ctx)
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 30ec7c19..24d16dca 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -127,9 +127,15 @@ let mk_struct_constructor (type_name : string) : string =
     a type parameter for the allocator to use, which we want to filter.
  *)
 let builtin_types () : builtin_type_info list =
-  let mk_type (rust_name : string) ?(keep_params : bool list option = None)
+  let mk_type (rust_name : string) ?(custom_name : string option = None)
+      ?(keep_params : bool list option = None)
       ?(kind : type_variant_kind = KOpaque) () : builtin_type_info =
-    let extract_name = flatten_name (split_on_separator rust_name) in
+    let rust_name = parse_pattern rust_name in
+    let extract_name =
+      match custom_name with
+      | None -> flatten_name (pattern_to_type_extract_name rust_name)
+      | Some name -> flatten_name (split_on_separator name)
+    in
     let body_info : builtin_type_body_info option =
       match kind with
       | KOpaque -> None
@@ -147,13 +153,16 @@ let builtin_types () : builtin_type_info list =
           Some (Struct (constructor, fields))
       | KEnum -> raise (Failure "TODO")
     in
-    let rust_name = parse_pattern rust_name in
     { rust_name; extract_name; keep_params; body_info }
   in
 
   [
     (* Alloc *)
     mk_type "alloc::alloc::Global" ();
+    (* String *)
+    mk_type "alloc::string::String"
+      ~custom_name:(Some (backend_choice "string" "String"))
+      ();
     (* Vec *)
     mk_type "alloc::vec::Vec" ~keep_params:(Some [ true; false ]) ();
     (* Range *)
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 41c81207..a916bffb 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -61,7 +61,10 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
               | TArray -> "Array"
               | TSlice -> "Slice"
             else expr_to_string c ty
-        | ERef _ | EVar _ -> raise (Failure ""))
+        | ERef _ | EVar _ ->
+            (* We simply convert the pattern to a string. This is not very
+               satisfying but we should rarely get there. *)
+            expr_to_string c ty)
   in
   let rec pattern_to_string (n : pattern) : string list =
     match n with
@@ -73,6 +76,7 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
   in
   pattern_to_string name
 
+let pattern_to_type_extract_name = pattern_to_extract_name false
 let pattern_to_fun_extract_name = pattern_to_extract_name false
 let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
 
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index c6212d31..ca9984be 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -213,7 +213,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool =
     - in Lean, groups of mutually recursive definitions must end with "end"
     - in HOL4 (in most situations) the whole group must be within a `Define` command
 
-    Calls to {!extract_fun_decl} should be inserted between calls to
+    Calls to {!Extract.extract_fun_decl} should be inserted between calls to
     {!start_fun_decl_group} and {!end_fun_decl_group}.
 
     TODO: maybe those [{start/end}_decl_group] functions are not that much a good
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 8c9c0e72..2f793f4a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -2155,7 +2155,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
      ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1));
 
   (* Check that the abstractions are destructured *)
-  if !Config.check_invariants then (
+  if !Config.sanity_checks then (
     let destructure_shared_values = true in
     assert (abs_is_destructured destructure_shared_values ctx abs0);
     assert (abs_is_destructured destructure_shared_values ctx abs1));
@@ -2487,7 +2487,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
   in
 
   (* Sanity check *)
-  if !Config.check_invariants then assert (abs_is_destructured true ctx abs);
+  if !Config.sanity_checks then assert (abs_is_destructured true ctx abs);
   (* Return *)
   abs
 
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index b13d545c..44f85d0a 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -924,7 +924,7 @@ let remove_intersecting_aproj_borrows_shared (regions : RegionId.Set.t)
         
     [subst]: takes as parameters the abstraction in which we perform the
     substitution and the list of given back values at the projector of
-    loans where we perform the substitution (see the fields in {!AProjLoans}).
+    loans where we perform the substitution (see the fields in {!Values.AProjLoans}).
     Note that the symbolic value at this place is necessarily equal to [sv],
     which is why we don't give it as parameters.
  *)
@@ -970,13 +970,13 @@ let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t)
   (* Return *)
   ctx
 
-(** Helper function: lookup an {!AProjLoans} by using an abstraction id and a
+(** Helper function: lookup an {!constructor:Values.aproj.AProjLoans} by using an abstraction id and a
     symbolic value.
-    
+
     We return the information from the looked up projector of loans. See the
-    fields in {!AProjLoans} (we don't return the symbolic value, because it
+    fields in {!constructor:Values.aproj.AProjLoans} (we don't return the symbolic value, because it
     is equal to [sv]).
-    
+
     Sanity check: we check that there is exactly one projector which corresponds
     to the couple (abstraction id, symbolic value).
  *)
@@ -1115,7 +1115,7 @@ let update_aproj_borrows (abs_id : AbstractionId.id) (sv : symbolic_value)
 
 (** Helper function: might break invariants.
 
-    Converts an {!AProjLoans} to an {!AEndedProjLoans}. The projector is identified
+    Converts an {!Values.aproj.AProjLoans} to an {!Values.aproj.AEndedProjLoans}. The projector is identified
     by a symbolic value and an abstraction id.
  *)
 let update_aproj_loans_to_ended (abs_id : AbstractionId.id)
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index 4be1fd24..b545f979 100644
--- a/compiler/InterpreterExpansion.mli
+++ b/compiler/InterpreterExpansion.mli
@@ -79,6 +79,6 @@ val expand_symbolic_int :
   m_fun
 
 (** If this mode is activated through the [config], greedily expand the symbolic
-    values which need to be expanded. See {!type:config} for more information.
+    values which need to be expanded. See {!type:Contexts.config} for more information.
  *)
 val greedy_expand_symbolic_values : config -> cm_fun
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index d14230c6..ca1f8f31 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -41,10 +41,10 @@ type abs_borrows_loans_maps = {
   borrow_loan_to_abs : AbstractionId.Set.t BorrowId.Map.t;
 }
 
-(** See {!InterpreterLoopsMatchCtxs.MakeMatcher} and {!InterpreterLoopsCore.Matcher}.
+(** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher].
 
     This module contains primitive match functions to instantiate the generic
-    {!InterpreterLoopsMatchCtxs.MakeMatcher} functor.
+    {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} functor.
   *)
 module type PrimMatcher = sig
   val match_etys : ety -> ety -> ety
@@ -231,8 +231,8 @@ module type Matcher = sig
     eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
 end
 
-(** See {!InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
-    {!InterpreterLoopsCore.CheckEquivMatcher}.
+(** See {!module:InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
+    {!module-type:InterpreterLoopsCore.CheckEquivMatcher}.
 
     Very annoying: functors only take modules as inputs...
  *)
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 4cc74aae..8d485483 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -714,7 +714,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id)
         ^ eval_ctx_to_string !joined_ctx));
 
     (* Sanity check *)
-    if !Config.check_invariants then Invariants.check_invariants !joined_ctx;
+    if !Config.sanity_checks then Invariants.check_invariants !joined_ctx;
     (* Return *)
     ctx1
   in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 74f9ba2c..bf459e41 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -1580,7 +1580,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
        ^ eval_ctx_to_string tgt_ctx));
 
     (* Sanity check *)
-    if !Config.check_invariants then
+    if !Config.sanity_checks then
       Invariants.check_borrowed_values_invariant tgt_ctx;
 
     (* End all the borrows which appear in the *new* abstractions *)
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index bf29af79..5f69b8d3 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -27,13 +27,13 @@ val compute_abs_borrows_loans_maps :
     We use it for joins, to check if two environments are convertible, etc.
     See for instance {!MakeJoinMatcher} and {!MakeCheckEquivMatcher}.
 
-    The functor is parameterized by a {!PrimMatcher}, which implements the
-    non-generic part of the match. More precisely, the role of {!PrimMatcher} is two
+    The functor is parameterized by a {!module-type:InterpreterLoopsCore.PrimMatcher}, which implements the
+    non-generic part of the match. More precisely, the role of {!module-type:InterpreterLoopsCore.PrimMatcher} is two
     provide generic functions which recursively match two values (by recursively
     matching the fields of ADT values for instance). When it does need to match
     values in a non-trivial manner (if two ADT values don't have the same
     variant for instance) it calls the corresponding specialized function from
-    {!PrimMatcher}.
+    {!module-type:InterpreterLoopsCore.PrimMatcher}.
  *)
 module MakeMatcher : functor (_ : PrimMatcher) -> Matcher
 
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 729a3577..999b8ab0 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -311,7 +311,7 @@ let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) :
       (* Note that we ignore the new environment: it should be the same as the
          original one.
       *)
-      if !Config.check_invariants then
+      if !Config.sanity_checks then
         if ctx1 <> ctx then (
           let msg =
             "Unexpected environment update:\nNew environment:\n"
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index 583c6907..9e4ebc20 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -6,7 +6,7 @@ open Contexts
 
     Apply a proj_borrows on a shared borrow.
     Note that when projecting over shared values, we generate
-    {!type:abstract_shared_borrows}, not {!type:avalue}s.
+    {!type:Aeneas.Values.abstract_shared_borrows}, not {!type:Aeneas.Values.avalue}s.
 
     Parameters:
     [regions]
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index d84e8be6..3832d02f 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -10,7 +10,7 @@ open Cps
     dummy variables, after ending the proper borrows of course) but the return
     variable, move the return value out of the return variable, remove all the
     local variables (but preserve the abstractions!), remove the
-    {!constructor:env_elem.Frame} indicator delimiting the current frame and
+    {!constructor:Contexts.env_elem.EFrame} indicator delimiting the current frame and
     handle the return value to the continuation.
 
     If the boolean is false, we don't move the return value, and call the
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index ecd8f53f..bba88e9f 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -111,7 +111,7 @@ let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value =
 (** Create a loans projector value from a symbolic value.
     
     Checks if the projector will actually project some regions. If not,
-    returns {!AIgnored} ([_]).
+    returns {!Values.AIgnored} ([_]).
     
     TODO: update to handle 'static
  *)
@@ -238,7 +238,7 @@ let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t)
   let regions = ty_regions s.sv_ty in
   not (RegionId.Set.disjoint regions ended_regions)
 
-(** Check if a {!type:value} contains [⊥].
+(** Check if a {!type:Values.value} contains [⊥].
 
     Note that this function is very general: it also checks wether
     symbolic values contain already ended regions.
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index e0e3f354..fa0d7436 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -804,7 +804,7 @@ let check_symbolic_values (ctx : eval_ctx) : unit =
   M.iter check_info !infos
 
 let check_invariants (ctx : eval_ctx) : unit =
-  if !Config.check_invariants then (
+  if !Config.sanity_checks then (
     log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ctx));
     check_loans_borrows_relation_invariant ctx;
     check_borrowed_values_invariant ctx;
diff --git a/compiler/Main.ml b/compiler/Main.ml
index e350da8a..7f98f581 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -107,10 +107,10 @@ let () =
         Arg.Set split_files,
         " Split the definitions between different files for types, functions, \
          etc." );
-      ( "-no-check-inv",
-        Arg.Clear check_invariants,
-        " Deactivate the invariant sanity checks performed at every evaluation \
-         step. Dramatically increases speed." );
+      ( "-checks",
+        Arg.Set sanity_checks,
+        " Activate extensive sanity checks (warning: causes a ~100 times slow \
+         down)." );
       ( "-no-gen-lib-entry",
         Arg.Clear generate_lib_entry_point,
         " Do not generate the entry point file for the generated library (only \
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 50849df9..0ae83007 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -273,7 +273,7 @@ class virtual ['self] mapreduce_ty_base =
 
 type ty =
   | TAdt of type_id * generic_args
-      (** {!Adt} encodes ADTs and tuples and assumed types.
+      (** {!TAdt} encodes ADTs and tuples and assumed types.
 
           TODO: what about the ended regions? (ADTs may be parameterized
           with several region variables. When giving back an ADT value, we may
@@ -1064,7 +1064,7 @@ type trait_impl = {
   meta : meta;
   impl_trait : trait_decl_ref;
   llbc_impl_trait : Types.trait_decl_ref;
-      (** Same remark as for {llbc_generics}. *)
+      (** Same remark as for {!field:llbc_generics}. *)
   generics : generic_params;
   llbc_generics : Types.generic_params;
       (** We use the LLBC generics to generate "pretty" names, for instance
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6b0deb73..a5143f3c 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -195,7 +195,7 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig =
     We only look for outer monadic let-bindings.
     This is used when printing the branches of [if ... then ... else ...].
 
-    Rem.: this function will *fail* if there are {!constructor:Aeneas.Pure.expression.Loop}
+    Rem.: this function will *fail* if there are {!Pure.Loop}
     nodes (you should call it on an expression where those nodes have been eliminated).
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 73e7f71d..a05b2c5a 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -76,7 +76,7 @@ let erase_regions_subst : subst =
     tr_self = Self;
   }
 
-(** Convert an {!rty} to an {!ety} by erasing the region variables *)
+(** Erase the region variables in a type *)
 let erase_regions (ty : ty) : ty = ty_substitute erase_regions_subst ty
 
 let trait_ref_erase_regions (tr : trait_ref) : trait_ref =
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index a9f45926..53f99b7f 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -66,8 +66,8 @@ type 'a region_group_id_map = 'a RegionGroupId.Map.t [@@deriving show]
 
 (** Ancestor for {!expression} iter visitor.
 
-    We could make it inherit the visitor for {!eval_ctx}, but in all the uses
-    of this visitor we don't need to explore {!eval_ctx}, so we make it inherit
+    We could make it inherit the visitor for {!Contexts.eval_ctx}, but in all the uses
+    of this visitor we don't need to explore {!Contexts.eval_ctx}, so we make it inherit
     the abstraction visitors instead.
  *)
 class ['self] iter_expression_base =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 05e48af5..37f58140 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -481,9 +481,19 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
       defs
   in
 
+  let dont_extract (d : Pure.type_decl) : bool =
+    match d.kind with
+    | Enum _ | Struct _ -> not config.extract_transparent
+    | Opaque -> not config.extract_opaque
+  in
+
   if List.exists (fun b -> b) builtin then
     (* Sanity check *)
     assert (List.for_all (fun b -> b) builtin)
+  else if List.exists dont_extract defs then
+    (* Check if we have to ignore declarations *)
+    (* Sanity check *)
+    assert (List.for_all dont_extract defs)
   else (
     (* Extract the type declarations.
 
@@ -873,6 +883,7 @@ type extract_file_info = {
   filename : string;
   namespace : string;
   in_namespace : bool;
+  open_namespace : bool;
   crate_name : string;
   rust_module_name : string;
   module_name : string;
@@ -931,8 +942,22 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       (* Add the custom includes *)
       List.iter
         (fun m ->
-          Printf.fprintf out "Require Export %s.\n" m;
-          Printf.fprintf out "Import %s.\n" m)
+          (* TODO: I don't really understand how the "Require Export",
+             "Require Import", "Include" work.
+             I used to have:
+             {[
+               Require Export %s.
+               Import %s.
+             ]}
+
+             I now have:
+             {[
+               Require Import %s.
+               Include %s.
+             ]}
+          *)
+          Printf.fprintf out "Require Import %s.\n" m;
+          Printf.fprintf out "Include %s.\n" m)
         fi.custom_includes;
       Printf.fprintf out "Module %s.\n" fi.module_name
   | Lean ->
@@ -943,9 +968,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes;
       (* Always open the Primitives namespace *)
       Printf.fprintf out "open Primitives\n";
-      (* If we are inside the namespace: declare it, otherwise: open it *)
-      if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace
-      else Printf.fprintf out "open %s\n" fi.namespace
+      (* If we are inside the namespace: declare it *)
+      if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace;
+      (* We might need to open the namespace *)
+      if fi.open_namespace then Printf.fprintf out "open %s\n" fi.namespace
   | HOL4 ->
       Printf.fprintf out "open primitivesLib divDefLib\n";
       (* Add the custom imports and includes *)
@@ -977,7 +1003,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   | FStar -> ()
   | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
   | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
-  | Coq -> Printf.fprintf out "End %s .\n" fi.module_name);
+  | Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
 
   (* Some logging *)
   log#linfo (lazy ("Generated: " ^ fi.filename));
@@ -1180,20 +1206,27 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     match primitives_src_dest with
     | None -> ()
     | Some (primitives_src, primitives_destname) -> (
-        let src = open_in (exe_dir ^ primitives_src) in
-        let tgt_filename = Filename.concat dest_dir primitives_destname in
-        let tgt = open_out tgt_filename in
-        (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
         try
-          while true do
-            (* We copy line by line *)
-            let line = input_line src in
-            Printf.fprintf tgt "%s\n" line
-          done
-        with End_of_file ->
-          close_in src;
-          close_out tgt;
-          log#linfo (lazy ("Copied:    " ^ tgt_filename)))
+          (* TODO: stop copying the primitives file *)
+          let src = open_in (exe_dir ^ primitives_src) in
+          let tgt_filename = Filename.concat dest_dir primitives_destname in
+          let tgt = open_out tgt_filename in
+          (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
+          try
+            while true do
+              (* We copy line by line *)
+              let line = input_line src in
+              Printf.fprintf tgt "%s\n" line
+            done
+          with End_of_file ->
+            close_in src;
+            close_out tgt;
+            log#linfo (lazy ("Copied:    " ^ tgt_filename))
+        with Sys_error _ ->
+          log#error
+            "Could not copy the primitives file: %s.\n\
+             You will have to copy it/set up the project by hand."
+            primitives_src)
   in
 
   (* Extract the file(s) *)
@@ -1250,12 +1283,72 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
      in
      let has_opaque_types = has_opaque_types || !Config.use_state in
 
-     (* Extract the types *)
+     (*
+      * Extract the types
+      *)
      (* If there are opaque types, we extract in an interface *)
-     (* TODO: for Lean and Coq: generate a template file *)
+     (* Extract the opaque type declarations, if needed *)
+     let opaque_types_module =
+       if has_opaque_types then (
+         (* For F*, we generate an .fsti, and let the user write the .fst.
+            For the other backends, we generate a template file as a model
+            for the file the user has to provide. *)
+         let module_suffix, opaque_imported_suffix, custom_msg =
+           match !Config.backend with
+           | FStar ->
+               ("TypesExternal", "TypesExternal", ": external type declarations")
+           | HOL4 | Coq | Lean ->
+               ( (* The name of the file we generate *)
+                 "TypesExternal_Template",
+                 (* The name of the file that will be imported by the Types
+                    module, and that the user has to provide. *)
+                 "TypesExternal",
+                 ": external types.\n\
+                  -- This is a template file: rename it to \
+                  \"TypesExternal.lean\" and fill the holes." )
+         in
+         let opaque_filename =
+           extract_filebasename ^ file_delimiter ^ module_suffix ^ opaque_ext
+         in
+         let opaque_module = crate_name ^ module_delimiter ^ module_suffix in
+         let opaque_imported_module =
+           crate_name ^ module_delimiter ^ opaque_imported_suffix
+         in
+         let opaque_config =
+           {
+             base_gen_config with
+             extract_opaque = true;
+             extract_transparent = false;
+             extract_types = true;
+             extract_trait_decls = true;
+             extract_state_type = !Config.use_state;
+             interface = true;
+           }
+         in
+         let file_info =
+           {
+             filename = opaque_filename;
+             namespace;
+             in_namespace = false;
+             open_namespace = false;
+             crate_name;
+             rust_module_name = crate.name;
+             module_name = opaque_module;
+             custom_msg;
+             custom_imports = [];
+             custom_includes = [];
+           }
+         in
+         extract_file opaque_config ctx file_info;
+         (* Return the additional dependencies *)
+         [ opaque_imported_module ])
+       else []
+     in
+
+     (* Extract the non opaque types *)
      let types_filename_ext =
        match !Config.backend with
-       | FStar -> if has_opaque_types then ".fsti" else ".fst"
+       | FStar -> ".fst"
        | Coq -> ".v"
        | Lean -> ".lean"
        | HOL4 -> "Script.sml"
@@ -1269,8 +1362,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          base_gen_config with
          extract_types = true;
          extract_trait_decls = true;
-         extract_opaque = true;
-         extract_state_type = !Config.use_state;
+         extract_opaque = false;
          interface = has_opaque_types;
        }
      in
@@ -1279,12 +1371,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          filename = types_filename;
          namespace;
          in_namespace = true;
+         open_namespace = false;
          crate_name;
          rust_module_name = crate.name;
          module_name = types_module;
          custom_msg = ": type definitions";
          custom_imports = [];
-         custom_includes = [];
+         custom_includes = opaque_types_module;
        }
      in
      extract_file types_config ctx file_info;
@@ -1307,6 +1400,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
             filename = template_clauses_filename;
             namespace;
             in_namespace = true;
+            open_namespace = false;
             crate_name;
             rust_module_name = crate.name;
             module_name = template_clauses_module;
@@ -1317,16 +1411,23 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
         in
         extract_file template_clauses_config ctx file_info);
 
-     (* Extract the opaque declarations, if needed *)
+     (* Extract the opaque fun declarations, if needed *)
      let opaque_funs_module =
        if has_opaque_funs then (
-         (* In the case of Lean we generate a template file *)
+         (* For F*, we generate an .fsti, and let the user write the .fst.
+            For the other backends, we generate a template file as a model
+            for the file the user has to provide. *)
          let module_suffix, opaque_imported_suffix, custom_msg =
            match !Config.backend with
-           | FStar | Coq | HOL4 ->
-               ("Opaque", "Opaque", ": external function declarations")
-           | Lean ->
-               ( "FunsExternal_Template",
+           | FStar ->
+               ( "FunsExternal",
+                 "FunsExternal",
+                 ": external function declarations" )
+           | HOL4 | Coq | Lean ->
+               ( (* The name of the file we generate *)
+                 "FunsExternal_Template",
+                 (* The name of the file that will be imported by the Funs
+                    module, and that the user has to provide. *)
                  "FunsExternal",
                  ": external functions.\n\
                   -- This is a template file: rename it to \
@@ -1337,9 +1438,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          in
          let opaque_module = crate_name ^ module_delimiter ^ module_suffix in
          let opaque_imported_module =
-           if !Config.backend = Lean then
-             crate_name ^ module_delimiter ^ opaque_imported_suffix
-           else opaque_module
+           crate_name ^ module_delimiter ^ opaque_imported_suffix
          in
          let opaque_config =
            {
@@ -1357,6 +1456,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
              filename = opaque_filename;
              namespace;
              in_namespace = false;
+             open_namespace = true;
              crate_name;
              rust_module_name = crate.name;
              module_name = opaque_module;
@@ -1396,6 +1496,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          filename = fun_filename;
          namespace;
          in_namespace = true;
+         open_namespace = false;
          crate_name;
          rust_module_name = crate.name;
          module_name = fun_module;
@@ -1429,6 +1530,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          filename = extract_filebasename ^ ext;
          namespace;
          in_namespace = true;
+         open_namespace = false;
          crate_name;
          rust_module_name = crate.name;
          module_name = crate_name;
diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
index 52e12b9a..76cc710a 100644
--- a/compiler/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
@@ -5,7 +5,7 @@ include Charon.TypesUtils
 (** Retuns true if the type contains borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
-    we erase the lists of regions (by replacing them with [[]] when using {!Types.ety},
+    we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty},
     and when a type uses 'static this region doesn't appear in the region parameters.
  *)
 let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
@@ -15,7 +15,7 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
 (** Retuns true if the type contains nested borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
-    we erase the lists of regions (by replacing them with [[]] when using {!Types.ety},
+    we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty},
     and when a type uses 'static this region doesn't appear in the region parameters.
  *)
 let ty_has_nested_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
diff --git a/flake.lock b/flake.lock
index 3457101c..8a34cfcb 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,11 +8,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1700661241,
-        "narHash": "sha256-vsMlaH7A5S7+uQGIYtu7Zt81s177X/xWbj2wdu54mtI=",
+        "lastModified": 1701097924,
+        "narHash": "sha256-fIXlINGdx8228emfCSkbqLN7f6mrLvoJc4gmqcyACU0=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "a3b93d7b6546f1501d5376f7c8bdc0d95d289eb6",
+        "rev": "a635cdc69aa3c17e06ebc42e0694b0fcb7fa0fbb",
         "type": "github"
       },
       "original": {
@@ -131,11 +131,11 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1700586754,
-        "narHash": "sha256-SfzRprm7aIqT4RYaOt5k/I0tCJwoCbdjRzr//2omX60=",
+        "lastModified": 1700646441,
+        "narHash": "sha256-yZe9nDY+0nAWATQLorXSJB7yZ6yNyIlz9mT/qxHgNac=",
         "owner": "fstarlang",
         "repo": "fstar",
-        "rev": "71f2d632e318996f227063bf9d31ee91a4f48dfe",
+        "rev": "fe6dec16fc4f0234663da63de26d9d2e72fe14df",
         "type": "github"
       },
       "original": {
@@ -164,11 +164,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1700602420,
-        "narHash": "sha256-RqTzTPk4c3hs9Z4IODcw/73L77Mo2tIPWw2KQzLv/O4=",
+        "lastModified": 1700661621,
+        "narHash": "sha256-XON6e4x5QRviofMGRyEwd+5PTVWAp/LdFFveC0LQhkY=",
         "owner": "hacl-star",
         "repo": "hacl-star",
-        "rev": "a5604d1b255e54cd32a104616c4b01808d46d809",
+        "rev": "95112e8dcb1ea3fe7d254290f8864b8f8e2fb6b2",
         "type": "github"
       },
       "original": {
@@ -194,11 +194,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1700615900,
-        "narHash": "sha256-dnhIrg55enqH2KteebnDoRRi4CRXX3y8UNorGzf1ofE=",
+        "lastModified": 1700702143,
+        "narHash": "sha256-BadYV0m36o3T0I7gB8rp7vos2HL6N+9I23+HAZdoZFM=",
         "owner": "hacl-star",
         "repo": "hacl-nix",
-        "rev": "7363c6f54bf89ccd5c968f4766c6ea19079b2661",
+        "rev": "84b572dc55ec16eb8403ada9934987fd7ff44f76",
         "type": "github"
       },
       "original": {
@@ -265,11 +265,11 @@
         "nixpkgs": "nixpkgs_4"
       },
       "locked": {
-        "lastModified": 1700650599,
-        "narHash": "sha256-AK9AO8COmeBpBFmhM9YLrAz/S7XknokCdXLIDC7tfQc=",
+        "lastModified": 1701086558,
+        "narHash": "sha256-Y5d0Ba09Bs8J6rxfH9gTEWEZ/pqDfIPwg73VYWpxIs8=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "9efdde23e0858f0925f0d3b4a6df842670b626c9",
+        "rev": "9769ad65723866093b35cd2c8875cc45e65d477a",
         "type": "github"
       },
       "original": {
@@ -318,11 +318,11 @@
         "nixpkgs": "nixpkgs_7"
       },
       "locked": {
-        "lastModified": 1700650599,
-        "narHash": "sha256-AK9AO8COmeBpBFmhM9YLrAz/S7XknokCdXLIDC7tfQc=",
+        "lastModified": 1701086558,
+        "narHash": "sha256-Y5d0Ba09Bs8J6rxfH9gTEWEZ/pqDfIPwg73VYWpxIs8=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "9efdde23e0858f0925f0d3b4a6df842670b626c9",
+        "rev": "9769ad65723866093b35cd2c8875cc45e65d477a",
         "type": "github"
       },
       "original": {
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 8e48b17d..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_Opaque.
-Import BetreeMain_Opaque.
+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_Opaque.v b/tests/coq/betree/BetreeMain_FunsExternal.v
index a065c8a3..07dba263 100644
--- a/tests/coq/betree/BetreeMain_Opaque.v
+++ b/tests/coq/betree/BetreeMain_FunsExternal.v
@@ -1,5 +1,6 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external function declarations *)
+(** [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.
@@ -8,7 +9,7 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export BetreeMain_Types.
 Import BetreeMain_Types.
-Module BetreeMain_Opaque.
+Module BetreeMain_FunsExternal.
 
 (** [betree_main::betree_utils::load_internal_node]: forward function
     Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
@@ -42,4 +43,4 @@ Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
 
-End BetreeMain_Opaque .
+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..36022a20
--- /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 Import BetreeMain_Types.
+Include 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_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 42c62421..13e4b9c1 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -4,6 +4,9 @@
 -arg all
 
 BetreeMain_Types.v
+BetreeMain_TypesExternal_Template.v
 Primitives.v
+BetreeMain_FunsExternal_Template.v
 BetreeMain_Funs.v
-BetreeMain_Opaque.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 46d3ee29..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_Opaque.
-Import HashmapMain_Opaque.
+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_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
index a0e9003d..a03dc407 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
@@ -8,7 +8,7 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export HashmapMain_Types.
 Import HashmapMain_Types.
-Module HashmapMain_Opaque.
+Module HashmapMain_FunsExternal.
 
 (** [hashmap_main::hashmap_utils::deserialize]: forward function
     Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
@@ -22,4 +22,4 @@ Axiom hashmap_utils_serialize
   : hashmap_HashMap_t u64 -> state -> result (state * unit)
 .
 
-End HashmapMain_Opaque .
+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..e10d02f6
--- /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 Import HashmapMain_Types.
+Include 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_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 b78c7b5f..41945494 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -6,4 +6,7 @@
 HashmapMain_Types.v
 Primitives.v
 HashmapMain_Funs.v
-HashmapMain_Opaque.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 0a14c7d1..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_Opaque.
-Import External_Opaque.
+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_Opaque.v b/tests/coq/misc/External_FunsExternal.v
index b482431f..a8c5756a 100644
--- a/tests/coq/misc/External_Opaque.v
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -7,8 +7,8 @@ Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export External_Types.
-Import External_Types.
-Module External_Opaque.
+Include External_Types.
+Module External_FunsExternal.
 
 (** [core::mem::swap]: forward function
     Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
@@ -40,4 +40,4 @@ Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
 
-End External_Opaque .
+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..31e69c39
--- /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 Import External_Types.
+Include 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_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 db6c2742..0828bced 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -4,11 +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_Opaque.v
-Paper.v
+External_FunsExternal.v
+External_TypesExternal_Template.v
+External_FunsExternal_Template.v
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 0952a1df..ebdca4ec 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
 .
@@ -617,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.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_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
index b89c8718..cd2f956f 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
@@ -1,6 +1,6 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
 (** [betree_main]: external function declarations *)
-module BetreeMain.Opaque
+module BetreeMain.FunsExternal
 open Primitives
 include BetreeMain.Types
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fst
index a098ec19..b87219b2 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
+++ b/tests/fstar/betree/BetreeMain.Types.fst
@@ -2,6 +2,7 @@
 (** [betree_main]: type definitions *)
 module BetreeMain.Types
 open Primitives
+include BetreeMain.TypesExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
@@ -58,6 +59,3 @@ type betree_BeTree_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.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/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
index b89c8718..cd2f956f 100644
--- a/tests/fstar/betree/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
@@ -1,6 +1,6 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
 (** [betree_main]: external function declarations *)
-module BetreeMain.Opaque
+module BetreeMain.FunsExternal
 open Primitives
 include BetreeMain.Types
 
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
index a098ec19..b87219b2 100644
--- a/tests/fstar/betree/BetreeMain.Types.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
@@ -2,6 +2,7 @@
 (** [betree_main]: type definitions *)
 module BetreeMain.Types
 open Primitives
+include BetreeMain.TypesExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
@@ -58,6 +59,3 @@ type betree_BeTree_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.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.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
index 1f47eb33..b00bbcde 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
@@ -1,6 +1,6 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
 (** [hashmap_main]: external function declarations *)
-module HashmapMain.Opaque
+module HashmapMain.FunsExternal
 open Primitives
 include HashmapMain.Types
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
index e77954ad..afebcde3 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
@@ -2,6 +2,7 @@
 (** [hashmap_main]: type definitions *)
 module HashmapMain.Types
 open Primitives
+include HashmapMain.TypesExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
@@ -21,6 +22,3 @@ type hashmap_HashMap_t (t : Type0) =
   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.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.Opaque.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index ea1a70c2..923a1101 100644
--- a/tests/fstar/misc/External.Opaque.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -1,6 +1,6 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
 (** [external]: external function declarations *)
-module External.Opaque
+module External.FunsExternal
 open Primitives
 include External.Types
 
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.TypesExternal.fsti
index 0cb9fd0e..4bfbe0c5 100644
--- a/tests/fstar/misc/External.Types.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -1,6 +1,6 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: type definitions *)
-module External.Types
+(** [external]: external type declarations *)
+module External.TypesExternal
 open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
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/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/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/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/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/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
+
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