From c61b32393508479657b51b777a0b4816815a55a5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 31 Aug 2023 19:10:00 +0200
Subject: Make progress on Extract and ExtractBase

---
 compiler/Config.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index bd80769f..ccbb4c75 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -323,3 +323,11 @@ let wrap_opaque_in_sig = ref false
     information), we use short names (i.e., the original field names).
  *)
 let record_fields_short_names = ref false
+
+(** Parameterize the traits with their associated types, so as not to use
+    types as first class objects.
+
+    This is useful for some backends with limited expressiveness like HOL4,
+    and to account for type constraints (like [fn f<T : Foo>(...) where T::bar = usize]).
+ *)
+let parameterize_trait_types = ref false
-- 
cgit v1.3.1


From d556b2439ad858fbbf612f433d25363a8f4a7c83 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Sep 2023 18:43:23 +0200
Subject: Fix more issues

---
 compiler/AssociatedTypes.ml | 90 ++++++++++++++++++++++++++++++++++++++++++---
 compiler/Config.ml          |  8 ++++
 compiler/Print.ml           | 22 +++++++++++
 compiler/SymbolicToPure.ml  | 77 +++++++++++++++++++++-----------------
 4 files changed, 157 insertions(+), 40 deletions(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index c4a9538d..bce0fb11 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -15,6 +15,7 @@ module C = Contexts
 module Subst = Substitute
 module L = Logging
 module UF = UnionFind
+module PA = Print.EvalCtxLlbcAst
 
 (** The local logger *)
 let log = L.associated_types_log
@@ -111,6 +112,10 @@ type 'r norm_ctx = {
   get_ty_repr : 'r C.trait_type_ref -> 'r T.ty option;
   convert_ety : T.ety -> 'r T.ty;
   convert_etrait_ref : T.etrait_ref -> 'r T.trait_ref;
+  ty_to_string : 'r T.ty -> string;
+  trait_ref_to_string : 'r T.trait_ref -> string;
+  trait_instance_id_to_string : 'r T.trait_instance_id -> string;
+  pp_r : Format.formatter -> 'r -> unit;
 }
 
 (** Normalize a type by simplyfying the references to trait associated types
@@ -118,6 +123,7 @@ type 'r norm_ctx = {
     enforced by local clauses (i.e., `where Trait1::T = Trait2::U`. *)
 let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty =
  fun ctx ty ->
+  log#ldebug (lazy ("ctx_normalize_ty: " ^ ctx.ty_to_string ty));
   match ty with
   | T.Adt (id, generics) -> Adt (id, ctx_normalize_generic_args ctx generics)
   | TypeVar _ | Literal _ | Never -> ty
@@ -125,19 +131,56 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty =
       let ty = ctx_normalize_ty ctx ty in
       T.Ref (r, ty, rkind)
   | TraitType (trait_ref, generics, type_name) -> (
+      log#ldebug
+        (lazy
+          ("ctx_normalize_ty: trait type: " ^ ctx.ty_to_string ty
+         ^ "\n- trait_ref: "
+          ^ ctx.trait_ref_to_string trait_ref
+          ^ "\n- raw trait ref: "
+          ^ T.show_trait_ref ctx.pp_r trait_ref));
       (* Normalize and attempt to project the type from the trait ref *)
       let trait_ref = ctx_normalize_trait_ref ctx trait_ref in
       let generics = ctx_normalize_generic_args ctx generics in
       let ty : 'r T.ty =
         match trait_ref.trait_id with
-        | T.TraitRef { T.trait_id = T.TraitImpl impl_id; generics; _ } ->
+        | T.TraitRef
+            { T.trait_id = T.TraitImpl impl_id; generics = ref_generics; _ } ->
+            assert (ref_generics = TypesUtils.mk_empty_generic_args);
+            log#ldebug
+              (lazy
+                ("ctx_normalize_ty: trait type: trait ref: "
+               ^ ctx.ty_to_string ty));
             (* Lookup the implementation *)
             let trait_impl = C.ctx_lookup_trait_impl ctx.ctx impl_id in
             (* Lookup the type *)
             let ty = snd (List.assoc type_name trait_impl.types) in
             (* Annoying: convert etype to an stype - TODO: hwo to avoid that? *)
             let ty : T.sty = TypesUtils.ety_no_regions_to_gr_ty ty in
-            (* Substitute - annoying: we can't use *)
+            (* Substitute *)
+            let tr_self = T.UnknownTrait __FUNCTION__ in
+            let subst =
+              Subst.make_subst_from_generics_no_regions trait_impl.generics
+                generics tr_self
+            in
+            let ty = Subst.ty_substitute subst ty in
+            (* Reconvert *)
+            let ty : 'r T.ty = ctx.convert_ety (Subst.erase_regions ty) in
+            (* Normalize *)
+            ctx_normalize_ty ctx ty
+        | T.TraitImpl impl_id ->
+            (* This happens. This doesn't come from the substituations
+               performed by Aeneas (the [TraitImpl] would be wrapped in a
+               [TraitRef] but from non-normalized traits translated from
+               the Rustc AST.
+               TODO: factor out with the branch above.
+            *)
+            (* Lookup the implementation *)
+            let trait_impl = C.ctx_lookup_trait_impl ctx.ctx impl_id in
+            (* Lookup the type *)
+            let ty = snd (List.assoc type_name trait_impl.types) in
+            (* Annoying: convert etype to an stype - TODO: hwo to avoid that? *)
+            let ty : T.sty = TypesUtils.ety_no_regions_to_gr_ty ty in
+            (* Substitute *)
             let tr_self = T.UnknownTrait __FUNCTION__ in
             let subst =
               Subst.make_subst_from_generics_no_regions trait_impl.generics
@@ -149,6 +192,13 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty =
             (* Normalize *)
             ctx_normalize_ty ctx ty
         | _ ->
+            log#ldebug
+              (lazy
+                ("ctx_normalize_ty: trait type: not a trait ref: "
+               ^ ctx.ty_to_string ty ^ "\n- trait_ref: "
+                ^ ctx.trait_ref_to_string trait_ref
+                ^ "\n- raw trait ref: "
+                ^ T.show_trait_ref ctx.pp_r trait_ref));
             (* We can't project *)
             assert (trait_instance_id_is_local_clause trait_ref.trait_id);
             T.TraitType (trait_ref, generics, type_name)
@@ -307,11 +357,31 @@ and ctx_normalize_generic_args (ctx : 'r norm_ctx)
 
 and ctx_normalize_trait_ref (ctx : 'r norm_ctx) (trait_ref : 'r T.trait_ref) :
     'r T.trait_ref =
+  log#ldebug
+    (lazy
+      ("ctx_normalize_trait_ref: "
+      ^ ctx.trait_ref_to_string trait_ref
+      ^ "\n- raw trait ref:\n"
+      ^ T.show_trait_ref ctx.pp_r trait_ref));
   let { T.trait_id; generics; trait_decl_ref } = trait_ref in
-  let trait_id, _ = ctx_normalize_trait_instance_id ctx trait_id in
-  let generics = ctx_normalize_generic_args ctx generics in
-  let trait_decl_ref = ctx_normalize_trait_decl_ref ctx trait_decl_ref in
-  { T.trait_id; generics; trait_decl_ref }
+  (* Check if the id is an impl, otherwise normalize it *)
+  let trait_id, norm_trait_ref = ctx_normalize_trait_instance_id ctx trait_id in
+  match norm_trait_ref with
+  | None ->
+      log#ldebug
+        (lazy
+          ("ctx_normalize_trait_ref: no norm: "
+          ^ ctx.trait_instance_id_to_string trait_id));
+      let generics = ctx_normalize_generic_args ctx generics in
+      let trait_decl_ref = ctx_normalize_trait_decl_ref ctx trait_decl_ref in
+      { T.trait_id; generics; trait_decl_ref }
+  | Some trait_ref ->
+      log#ldebug
+        (lazy
+          ("ctx_normalize_trait_ref: normalized to: "
+          ^ ctx.trait_ref_to_string trait_ref));
+      assert (generics = TypesUtils.mk_empty_generic_args);
+      trait_ref
 
 (* Not sure this one is really necessary *)
 and ctx_normalize_trait_decl_ref (ctx : 'r norm_ctx)
@@ -335,6 +405,10 @@ let mk_rnorm_ctx (ctx : C.eval_ctx) : T.RegionId.id T.region norm_ctx =
     get_ty_repr;
     convert_ety = TypesUtils.ety_no_regions_to_rty;
     convert_etrait_ref = TypesUtils.etrait_ref_no_regions_to_gr_trait_ref;
+    ty_to_string = PA.rty_to_string ctx;
+    trait_ref_to_string = PA.rtrait_ref_to_string ctx;
+    trait_instance_id_to_string = PA.rtrait_instance_id_to_string ctx;
+    pp_r = T.pp_region T.pp_region_id;
   }
 
 let mk_enorm_ctx (ctx : C.eval_ctx) : T.erased_region norm_ctx =
@@ -344,6 +418,10 @@ let mk_enorm_ctx (ctx : C.eval_ctx) : T.erased_region norm_ctx =
     get_ty_repr;
     convert_ety = (fun x -> x);
     convert_etrait_ref = (fun x -> x);
+    ty_to_string = PA.ety_to_string ctx;
+    trait_ref_to_string = PA.etrait_ref_to_string ctx;
+    trait_instance_id_to_string = PA.etrait_instance_id_to_string ctx;
+    pp_r = T.pp_erased_region;
   }
 
 let ctx_normalize_rty (ctx : C.eval_ctx) (ty : T.rty) : T.rty =
diff --git a/compiler/Config.ml b/compiler/Config.ml
index ccbb4c75..508746d9 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -331,3 +331,11 @@ let record_fields_short_names = ref false
     and to account for type constraints (like [fn f<T : Foo>(...) where T::bar = usize]).
  *)
 let parameterize_trait_types = ref false
+
+(** For sanity check: type check the generated pure code (activates checks in
+    several places).
+
+    TODO: deactivated for now because we need to implement the normalization of
+    trait associated types in the pure code.
+ *)
+let type_check_pure_code = ref false
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 92743bc1..93a1f970 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -651,6 +651,28 @@ module EvalCtxLlbcAst = struct
     let fmt = PC.ctx_to_rtype_formatter fmt in
     PT.rty_to_string fmt t
 
+  let etrait_ref_to_string (ctx : C.eval_ctx) (x : T.etrait_ref) : string =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_etype_formatter fmt in
+    PT.etrait_ref_to_string fmt x
+
+  let rtrait_ref_to_string (ctx : C.eval_ctx) (x : T.rtrait_ref) : string =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_rtype_formatter fmt in
+    PT.rtrait_ref_to_string fmt x
+
+  let etrait_instance_id_to_string (ctx : C.eval_ctx) (x : T.etrait_instance_id)
+      : string =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_etype_formatter fmt in
+    PT.etrait_instance_id_to_string fmt x
+
+  let rtrait_instance_id_to_string (ctx : C.eval_ctx) (x : T.rtrait_instance_id)
+      : string =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_rtype_formatter fmt in
+    PT.rtrait_instance_id_to_string fmt x
+
   let egeneric_args_to_string (ctx : C.eval_ctx) (x : T.egeneric_args) : string
       =
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4c5b99c3..2e0e9862 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -687,8 +687,9 @@ let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
   ()
 
 let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
-  let ctx = mk_type_check_ctx ctx in
-  PureTypeCheck.check_texpression ctx e
+  if !Config.type_check_pure_code then
+    let ctx = mk_type_check_ctx ctx in
+    PureTypeCheck.check_texpression ctx e
 
 let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
     (id : A.fun_id_or_trait_method_ref) : fun_id_or_trait_method_ref =
@@ -1817,9 +1818,11 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
   (* Group the two lists *)
   let variables_values = List.combine given_back_variables consumed_values in
   (* Sanity check: the two lists match (same types) *)
-  List.iter
-    (fun (var, v) -> assert ((var : var).ty = (v : texpression).ty))
-    variables_values;
+  (* TODO: normalize the types *)
+  if !Config.type_check_pure_code then
+    List.iter
+      (fun (var, v) -> assert ((var : var).ty = (v : texpression).ty))
+      variables_values;
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
   (* Generate the assignemnts *)
@@ -1892,31 +1895,35 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     | Some nstate -> mk_simpl_tuple_pattern [ nstate; output ]
   in
   (* Sanity check: there is the proper number of inputs and outputs, and they have the proper type *)
-  let _ =
-    let inst_sg = get_instantiated_fun_sig fun_id (Some rg_id) generics ctx in
-    log#ldebug
-      (lazy
-        ("\n- fun_id: " ^ A.show_fun_id fun_id ^ "\n- inputs ("
-        ^ string_of_int (List.length inputs)
-        ^ "): "
-        ^ String.concat ", " (List.map (texpression_to_string ctx) inputs)
-        ^ "\n- inst_sg.inputs ("
-        ^ string_of_int (List.length inst_sg.inputs)
-        ^ "): "
-        ^ String.concat ", " (List.map (ty_to_string ctx) inst_sg.inputs)));
-    List.iter
-      (fun (x, ty) -> assert ((x : texpression).ty = ty))
-      (List.combine inputs inst_sg.inputs);
-    log#ldebug
-      (lazy
-        ("\n- outputs: "
-        ^ string_of_int (List.length outputs)
-        ^ "\n- expected outputs: "
-        ^ string_of_int (List.length inst_sg.doutputs)));
-    List.iter
-      (fun (x, ty) -> assert ((x : typed_pattern).ty = ty))
-      (List.combine outputs inst_sg.doutputs)
-  in
+  (if (* TODO: normalize the types *) !Config.type_check_pure_code then
+     match fun_id with
+     | A.FunId fun_id ->
+         let inst_sg =
+           get_instantiated_fun_sig fun_id (Some rg_id) generics ctx
+         in
+         log#ldebug
+           (lazy
+             ("\n- fun_id: " ^ A.show_fun_id fun_id ^ "\n- inputs ("
+             ^ string_of_int (List.length inputs)
+             ^ "): "
+             ^ String.concat ", " (List.map (texpression_to_string ctx) inputs)
+             ^ "\n- inst_sg.inputs ("
+             ^ string_of_int (List.length inst_sg.inputs)
+             ^ "): "
+             ^ String.concat ", " (List.map (ty_to_string ctx) inst_sg.inputs)));
+         List.iter
+           (fun (x, ty) -> assert ((x : texpression).ty = ty))
+           (List.combine inputs inst_sg.inputs);
+         log#ldebug
+           (lazy
+             ("\n- outputs: "
+             ^ string_of_int (List.length outputs)
+             ^ "\n- expected outputs: "
+             ^ string_of_int (List.length inst_sg.doutputs)));
+         List.iter
+           (fun (x, ty) -> assert ((x : typed_pattern).ty = ty))
+           (List.combine outputs inst_sg.doutputs)
+     | _ -> (* TODO: trait methods *) ());
   (* Retrieve the function id, and register the function call in the context
    * if necessary *)
   let ctx, func =
@@ -2961,10 +2968,12 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
             ^ "\n- signature.inputs: "
             ^ String.concat ", " (List.map (ty_to_string ctx) signature.inputs)
             ));
-        assert (
-          List.for_all
-            (fun (var, ty) -> (var : var).ty = ty)
-            (List.combine inputs signature.inputs));
+        (* TODO: we need to normalize the types *)
+        if !Config.type_check_pure_code then
+          assert (
+            List.for_all
+              (fun (var, ty) -> (var : var).ty = ty)
+              (List.combine inputs signature.inputs));
         Some { inputs; inputs_lvs; body }
   in
 
-- 
cgit v1.3.1


From e8aa3804ef0134631cc16b257775ad8f98690c29 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 14 Sep 2023 00:42:46 +0200
Subject: Make progress on the extraction

---
 compiler/Config.ml      |  4 ++++
 compiler/Extract.ml     | 10 +++++++++-
 compiler/ExtractBase.ml | 16 +++++++++++-----
 3 files changed, 24 insertions(+), 6 deletions(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 508746d9..62f6c300 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -339,3 +339,7 @@ let parameterize_trait_types = ref false
     trait associated types in the pure code.
  *)
 let type_check_pure_code = ref false
+
+(** Shall we fail hard if there is an issue at code-generation time?
+    We may not want in case outputting a code with holes helps debugging *)
+let extract_fail_hard = ref false
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index fe007d31..864d513f 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -529,7 +529,15 @@ let type_decl_kind_to_qualif (kind : decl_kind)
            *)
           Some "with"
       | (Assumed | Declared), None -> Some "Axiom"
-      | _ -> raise (Failure "Unexpected"))
+      | SingleNonRec, None ->
+          (* This is for traits *)
+          Some "Record"
+      | _ ->
+          raise
+            (Failure
+               ("Unexpected: (" ^ show_decl_kind kind ^ ", "
+               ^ Print.option_to_string show_type_decl_kind type_kind
+               ^ ")")))
   | Lean -> (
       match kind with
       | SingleNonRec ->
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 6789b5b8..612cf359 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -78,6 +78,7 @@ type decl_kind =
           F*:  [val x : Type0]
           Coq: [Axiom x : Type.]
        *)
+[@@deriving show]
 
 (** Return [true] if the declaration is the last from its group of declarations.
 
@@ -112,7 +113,7 @@ let decl_is_first_from_group (kind : decl_kind) : bool =
 let decl_is_not_last_from_group (kind : decl_kind) : bool =
   not (decl_is_last_from_group kind)
 
-type type_decl_kind = Enum | Struct
+type type_decl_kind = Enum | Struct [@@deriving show]
 
 (* TODO: this should be a module we give to a functor! *)
 
@@ -533,7 +534,8 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
   | None -> () (* Ok *)
   | Some clash ->
       (* There is a clash: print a nice debugging message for the user *)
-      report_name_collision id_to_string clash id name
+      if !Config.extract_fail_hard then
+        report_name_collision id_to_string clash id name
 
 let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id)
     (name : string) (nm : names_map) : names_map =
@@ -707,9 +709,12 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
                 Print.fun_name_to_string
                   (A.FunDeclId.Map.find fid fun_decls).name
             | FunId (Assumed aid) -> A.show_assumed_fun_id aid
-            | TraitMethod _ ->
+            | TraitMethod (_, method_name, _) ->
                 (* Shouldn't happen *)
-                raise (Failure "Unexpected")
+                if !Config.extract_fail_hard then raise (Failure "Unexpected")
+                else (
+                  log#serror ("Unexpected trait method: " ^ method_name);
+                  method_name)
           in
 
           let lp_kind =
@@ -899,7 +904,8 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
         if with_opaque_pre && is_opaque then ctx.fmt.opaque_pre () ^ s else s
     | None ->
         log#serror ("Could not find: " ^ id_to_string id ctx);
-        raise Not_found
+        if !Config.extract_fail_hard then raise (Failure "Not found")
+        else "(ERROR: \"" ^ id_to_string id ctx ^ "\")"
 
 let ctx_get_global (with_opaque_pre : bool) (id : A.GlobalDeclId.id)
     (ctx : extraction_ctx) : string =
-- 
cgit v1.3.1


From b631875f8166b3db81187a179eef2f21f52db2bd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 15:26:41 +0200
Subject: Remove the possibility of generating opaque module signatures

---
 compiler/Config.ml      |   7 --
 compiler/Extract.ml     | 167 +++++++++++-----------------------
 compiler/ExtractBase.ml | 233 ++++++++++++------------------------------------
 compiler/Translate.ml   |  34 +------
 4 files changed, 111 insertions(+), 330 deletions(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 62f6c300..cd0903b6 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -306,13 +306,6 @@ let filter_useless_monadic_calls = ref true
  *)
 let filter_useless_functions = ref true
 
-(** Obsolete. TODO: remove.
-
-    For Lean we used to parameterize the entire development by a section variable
-    called opaque_defs, of type OpaqueDefs.
-  *)
-let wrap_opaque_in_sig = ref false
-
 (** Use short names for the record fields.
 
     Some backends can't disambiguate records when their field names have collisions.
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index a1c9605b..275cb3b9 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -758,12 +758,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     fname ^ lp_suffix ^ suffix
   in
 
-  let opaque_pre () =
-    match !Config.backend with
-    | FStar | Coq | HOL4 -> ""
-    | Lean -> if !Config.wrap_opaque_in_sig then "opaque_defs." else ""
-  in
-
   let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
       : string =
     (* Small helper to derive var names from ADT type names.
@@ -934,7 +928,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     trait_type_name;
     trait_method_name;
     trait_type_clause_name;
-    opaque_pre;
     var_basename;
     type_var_basename;
     const_generic_var_basename;
@@ -983,11 +976,8 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
       (* In HOL4, opaque functions have a special treatment *)
       if is_single_opaque_fun_decl_group dg then ()
       else
-        let with_opaque_pre = false in
         let compute_fun_def_name (def : Pure.fun_decl) : string =
-          ctx_get_local_function with_opaque_pre def.def_id def.loop_id
-            def.back_id ctx
-          ^ "_def"
+          ctx_get_local_function def.def_id def.loop_id def.back_id ctx ^ "_def"
         in
         let names = List.map compute_fun_def_name dg in
         (* Add a break before *)
@@ -1110,7 +1100,7 @@ let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
     (inside : bool) (cg : const_generic) : unit =
   match cg with
   | ConstGenericGlobal id ->
-      let s = ctx_get_global ctx.use_opaque_pre id ctx in
+      let s = ctx_get_global id ctx in
       F.pp_print_string fmt s
   | ConstGenericValue v -> ctx.fmt.extract_literal fmt inside v
   | ConstGenericVar id ->
@@ -1178,14 +1168,13 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
              In HOL4 we would write:
              `('a, 'b) tree`
           *)
-          let with_opaque_pre = false in
           match !backend with
           | FStar | Coq | Lean ->
               let print_paren = inside && has_params in
               if print_paren then F.pp_print_string fmt "(";
               (* TODO: for now, only the opaque *functions* are extracted in the
                  opaque module. The opaque *types* are assumed. *)
-              F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx);
+              F.pp_print_string fmt (ctx_get_type type_id ctx);
               extract_generic_args ctx fmt no_params_tys generics;
               if print_paren then F.pp_print_string fmt ")"
           | HOL4 ->
@@ -1208,7 +1197,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
                   (extract_rec true) types;
                 if print_paren then F.pp_print_string fmt ")";
                 F.pp_print_space fmt ());
-              F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx);
+              F.pp_print_string fmt (ctx_get_type type_id ctx);
               if trait_refs <> [] then (
                 F.pp_print_space fmt ();
                 Collections.List.iter_link (F.pp_print_space fmt)
@@ -1273,8 +1262,7 @@ and extract_trait_decl_ref (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_decl_ref) :
     unit =
   let use_brackets = tr.decl_generics <> empty_generic_args && inside in
-  let is_opaque = false in
-  let name = ctx_get_trait_decl is_opaque tr.trait_decl_id ctx in
+  let name = ctx_get_trait_decl tr.trait_decl_id ctx in
   if use_brackets then F.pp_print_string fmt "(";
   F.pp_print_string fmt name;
   (* There is something subtle here: the trait obligations for the implemented
@@ -1307,14 +1295,13 @@ and extract_generic_args (ctx : extraction_ctx) (fmt : F.formatter)
 and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (id : trait_instance_id)
     : unit =
-  let with_opaque_pre = false in
   match id with
   | Self ->
       (* This has specific treatment depending on the item we're extracting
          (associated type, etc.). We should have caught this elsewhere. *)
       raise (Failure "Unexpected")
   | TraitImpl id ->
-      let name = ctx_get_trait_impl with_opaque_pre id ctx in
+      let name = ctx_get_trait_impl id ctx in
       F.pp_print_string fmt name
   | Clause id ->
       let name = ctx_get_local_trait_clause id ctx in
@@ -1354,8 +1341,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
     | None -> ctx.fmt.type_name def.name
     | Some info -> String.concat "." info.rust_name
   in
-  let is_opaque = def.kind = Opaque in
-  let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in
+  let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
   (* Compute and register:
    * - the variant names, if this is an enumeration
    * - the field names, if this is a structure
@@ -1392,11 +1378,11 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
         let ctx =
           List.fold_left
             (fun ctx (fid, name) ->
-              ctx_add is_opaque (FieldId (AdtId def.def_id, fid)) name ctx)
+              ctx_add (FieldId (AdtId def.def_id, fid)) name ctx)
             ctx field_names
         in
         (* Add the constructor name *)
-        ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx
+        ctx_add (StructId (AdtId def.def_id)) cons_name ctx
     | Enum variants ->
         let variant_names =
           match info with
@@ -1432,7 +1418,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
         in
         List.fold_left
           (fun ctx (vid, vname) ->
-            ctx_add is_opaque (VariantId (AdtId def.def_id, vid)) vname ctx)
+            ctx_add (VariantId (AdtId def.def_id, vid)) vname ctx)
           ctx variant_names
     | Opaque ->
         (* Nothing to do *)
@@ -1635,9 +1621,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       (* If Coq: print the constructor name *)
       (* TODO: remove superfluous test not is_rec below *)
       if !backend = Coq && not is_rec then (
-        let with_opaque_pre = false in
-        F.pp_print_string fmt
-          (ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx);
+        F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx);
         F.pp_print_string fmt " ");
       (match !backend with
       | Lean -> ()
@@ -1681,16 +1665,14 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       (* We extract for Coq or Lean, and we have a recursive record, or a record in
          a group of mutually recursive types: we extract it as an inductive type *)
       assert (is_rec && (!backend = Coq || !backend = Lean));
-      let with_opaque_pre = false in
       (* Small trick: in Lean we use namespaces, meaning we don't need to prefix
          the constructor name with the name of the type at definition site,
          i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq
          we generate `inductive Foo := | mk ... *)
       let cons_name =
-        if !backend = Lean then "mk"
-        else ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx
+        if !backend = Lean then "mk" else ctx_get_struct (AdtId def.def_id) ctx
       in
-      let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+      let def_name = ctx_get_local_type def.def_id ctx in
       extract_type_decl_variant ctx fmt type_decl_group def_name type_params
         cg_params cons_name fields)
   in
@@ -1720,8 +1702,7 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
 
 let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
-  let with_opaque_pre = false in
-  let trait_name = ctx_get_trait_decl with_opaque_pre clause.trait_id ctx in
+  let trait_name = ctx_get_trait_decl clause.trait_id ctx in
   F.pp_print_string fmt trait_name;
   extract_generic_args ctx fmt no_params_tys clause.generics
 
@@ -1743,8 +1724,7 @@ let extract_trait_self_clause (insert_req_space : unit -> unit)
   F.pp_print_space fmt ();
   F.pp_print_string fmt ":";
   F.pp_print_space fmt ();
-  let with_opaque_pre = false in
-  let trait_id = ctx_get_trait_decl with_opaque_pre trait_decl.def_id ctx in
+  let trait_id = ctx_get_trait_decl trait_decl.def_id ctx in
   F.pp_print_string fmt trait_id;
   List.iter
     (fun p ->
@@ -1913,8 +1893,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   let is_opaque_coq = !backend = Coq && is_opaque in
   let use_forall = is_opaque_coq && def.generics <> empty_generic_params in
   (* Retrieve the definition name *)
-  let with_opaque_pre = false in
-  let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+  let def_name = ctx_get_local_type def.def_id ctx in
   (* Add the type and const generic params - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx_body, type_params, cg_params, trait_clauses =
@@ -2001,8 +1980,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
     (def : type_decl) : unit =
   (* Retrieve the definition name *)
-  let with_opaque_pre = false in
-  let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+  let def_name = ctx_get_local_type def.def_id ctx in
   (* Generic parameters are unsupported *)
   assert (def.generics.const_generics = []);
   (* Trait clauses on type definitions are unsupported *)
@@ -2027,8 +2005,7 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
     (fmt : F.formatter) (def : type_decl) : unit =
   (* Retrieve the definition name *)
-  let with_opaque_pre = false in
-  let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+  let def_name = ctx_get_local_type def.def_id ctx in
   (* Sanity check *)
   assert (def.generics = empty_generic_params);
   (* Generate the declaration *)
@@ -2111,8 +2088,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
     | Struct fields ->
         let adt_id = AdtId decl.def_id in
         (* Generate the instruction for the record constructor *)
-        let with_opaque_pre = false in
-        let cons_name = ctx_get_struct with_opaque_pre adt_id ctx in
+        let cons_name = ctx_get_struct adt_id ctx in
         extract_arguments_info cons_name fields;
         (* Generate the instruction for the record projectors, if there are *)
         let is_rec = decl_is_from_rec_group kind in
@@ -2156,11 +2132,8 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
         in
         let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in
         let ctx, field_var = ctx_add_var "x" (VarId.of_int 1) ctx in
-        let with_opaque_pre = false in
-        let def_name = ctx_get_local_type with_opaque_pre decl.def_id ctx in
-        let cons_name =
-          ctx_get_struct with_opaque_pre (AdtId decl.def_id) ctx
-        in
+        let def_name = ctx_get_local_type decl.def_id ctx in
+        let cons_name = ctx_get_struct (AdtId decl.def_id) ctx in
         let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
           F.pp_print_space fmt ();
           (* Outer box for the projector definition *)
@@ -2391,7 +2364,6 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
       | Some (_filter, info) ->
           let backs = List.map (fun f -> f.f) def.backs in
           let funs = if def.keep_fwd then def.fwd.f :: backs else backs in
-          let is_opaque = false in
           List.fold_left
             (fun ctx (f : fun_decl) ->
               let open ExtractBuiltin in
@@ -2404,7 +2376,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
                    info)
                   .extract_name
               in
-              ctx_add is_opaque (FunId (FromLlbc fun_id)) fun_name ctx)
+              ctx_add (FunId (FromLlbc fun_id)) fun_name ctx)
             ctx funs
       | None ->
           let fwd = def.fwd in
@@ -2509,18 +2481,14 @@ let extract_adt_g_value
          * [{ field0=...; ...; fieldn=...; }] in case of structures.
          *)
         let cons =
-          (* The ADT shouldn't be opaque *)
-          let with_opaque_pre = false in
           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, Assumed _ ->
-                  ctx_get_type with_opaque_pre adt_id ctx
-                  ^ "."
-                  ^ ctx_get_variant adt_id vid ctx
+                  ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx
               | _ -> ctx_get_variant adt_id vid ctx)
-          | None -> ctx_get_struct with_opaque_pre adt_id ctx
+          | None -> ctx_get_struct adt_id ctx
         in
         let use_parentheses = inside && field_values <> [] in
         if use_parentheses then F.pp_print_string fmt "(";
@@ -2539,8 +2507,7 @@ let extract_adt_g_value
 (* Extract globals in the same way as variables *)
 let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
     (id : A.GlobalDeclId.id) : unit =
-  let with_opaque_pre = ctx.use_opaque_pre in
-  F.pp_print_string fmt (ctx_get_global with_opaque_pre id ctx)
+  F.pp_print_string fmt (ctx_get_global id ctx)
 
 (** [inside]: see {!extract_ty}.
 
@@ -2676,9 +2643,9 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
       if inside then F.pp_print_string fmt "(";
       (* Open a box for the function call *)
       F.pp_open_hovbox fmt ctx.indent_incr;
-      (* Print the function name *)
-      let with_opaque_pre = ctx.use_opaque_pre in
-      (* For the function name: the id is not the same depending on whether
+      (* Print the function name.
+
+         For the function name: the id is not the same depending on whether
          we call a trait method and a "regular" function (remark: trait
          method *implementations* are considered as regular functions here;
          only calls to method of traits which are parameterized in a where
@@ -2751,7 +2718,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
             let fun_id =
               FromLlbc (FunId (Regular method_id.id), lp_id, rg_id)
             in
-            let fun_name = ctx_get_function with_opaque_pre fun_id ctx in
+            let fun_name = ctx_get_function fun_id ctx in
             F.pp_print_string fmt fun_name;
 
             (* Note that we do not need to print the generics for the trait
@@ -2762,7 +2729,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
             F.pp_print_space fmt ();
             extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref
       | _ ->
-          let fun_name = ctx_get_function with_opaque_pre fun_id ctx in
+          let fun_name = ctx_get_function fun_id ctx in
           F.pp_print_string fmt fun_name);
 
       (* Sanity check: HOL4 doesn't support const generics *)
@@ -3260,7 +3227,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
         (* Open the box for `Array.replicate T N [` *)
         F.pp_open_hovbox fmt ctx.indent_incr;
         (* Print the array constructor *)
-        let cs = ctx_get_struct false (Assumed Array) ctx in
+        let cs = ctx_get_struct (Assumed Array) ctx in
         F.pp_print_string fmt cs;
         (* Print the parameters *)
         let _, generics = ty_as_adt e_ty in
@@ -3613,10 +3580,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
   assert (not def.is_global_decl_body);
   (* Retrieve the function name *)
-  let with_opaque_pre = false in
   let def_name =
-    ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id
-      ctx
+    ctx_get_local_function def.def_id def.loop_id def.back_id ctx
   in
   (* Add a break before *)
   if !backend <> HOL4 || not (decl_is_first_from_group kind) then
@@ -3649,8 +3614,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
      if `wrap_opaque_in_sig`: we generate a record of assumed funcions.
      TODO: this is obsolete.
   *)
-  (if not (!Config.wrap_opaque_in_sig && (kind = Assumed || kind = Declared))
-   then
+  (if not (kind = Assumed || kind = Declared) then
      let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
      match qualif with
      | Some qualif ->
@@ -3867,10 +3831,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
     (def : fun_decl) : unit =
   (* Retrieve the definition name *)
-  let with_opaque_pre = false in
   let def_name =
-    ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id
-      ctx
+    ctx_get_local_function def.def_id def.loop_id def.back_id ctx
   in
   assert (def.signature.generics.const_generics = []);
   (* Add the type/const gen parameters - note that we need those bindings
@@ -4065,10 +4027,9 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
   extract_comment fmt [ "[" ^ Print.global_name_to_string global.name ^ "]" ];
   F.pp_print_space fmt ();
 
-  let with_opaque_pre = false in
-  let decl_name = ctx_get_global with_opaque_pre global.def_id ctx in
+  let decl_name = ctx_get_global global.def_id ctx in
   let body_name =
-    ctx_get_function with_opaque_pre
+    ctx_get_function
       (FromLlbc (Pure.FunId (Regular global.body_id), None, None))
       ctx
   in
@@ -4111,7 +4072,6 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
     (trait_decl : trait_decl)
     (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
     extraction_ctx =
-  let is_opaque = false in
   let generics = trait_decl.generics in
   (* Compute the clause names *)
   let clause_names =
@@ -4135,7 +4095,7 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
   (* Register the names *)
   List.fold_left
     (fun ctx (cid, cname) ->
-      ctx_add is_opaque (TraitParentClauseId (trait_decl.def_id, cid)) cname ctx)
+      ctx_add (TraitParentClauseId (trait_decl.def_id, cid)) cname ctx)
     ctx clause_names
 
 (** Similar to {!extract_trait_decl_register_names} *)
@@ -4143,7 +4103,6 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
     (trait_decl : trait_decl)
     (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
     extraction_ctx =
-  let is_opaque = false in
   let consts = trait_decl.consts in
   (* Compute the names *)
   let constant_names =
@@ -4169,7 +4128,7 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
   (* Register the names *)
   List.fold_left
     (fun ctx (item_name, name) ->
-      ctx_add is_opaque (TraitItemId (trait_decl.def_id, item_name)) name ctx)
+      ctx_add (TraitItemId (trait_decl.def_id, item_name)) name ctx)
     ctx constant_names
 
 (** Similar to {!extract_trait_decl_register_names} *)
@@ -4177,7 +4136,6 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
     (trait_decl : trait_decl)
     (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
     extraction_ctx =
-  let is_opaque = false in
   let types = trait_decl.types in
   (* Compute the names *)
   let type_names =
@@ -4227,13 +4185,11 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
   List.fold_left
     (fun ctx (item_name, (type_name, clauses)) ->
       let ctx =
-        ctx_add is_opaque
-          (TraitItemId (trait_decl.def_id, item_name))
-          type_name ctx
+        ctx_add (TraitItemId (trait_decl.def_id, item_name)) type_name ctx
       in
       List.fold_left
         (fun ctx (clause_id, clause_name) ->
-          ctx_add is_opaque
+          ctx_add
             (TraitItemClauseId (trait_decl.def_id, item_name, clause_id))
             clause_name ctx)
         ctx clauses)
@@ -4244,7 +4200,6 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
     (trait_decl : trait_decl)
     (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
     extraction_ctx =
-  let is_opaque = false in
   let required_methods = trait_decl.required_methods in
   (* Compute the names *)
   let method_names =
@@ -4305,7 +4260,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
       (* We add one field per required forward/backward function *)
       List.fold_left
         (fun ctx (rg, fun_name) ->
-          ctx_add is_opaque
+          ctx_add
             (TraitMethodId (trait_decl.def_id, item_name, rg))
             fun_name ctx)
         ctx funs)
@@ -4326,8 +4281,7 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
       | None -> ctx.fmt.trait_decl_name trait_decl
       | Some info -> info.extract_name
     in
-    let is_opaque = false in
-    ctx_add is_opaque (TraitDeclId trait_decl.def_id) trait_name ctx
+    ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx
   in
   (* Parent clauses *)
   let ctx =
@@ -4369,8 +4323,7 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
     | None -> ctx.fmt.trait_impl_name trait_decl trait_impl
     | Some name -> name
   in
-  let is_opaque = false in
-  ctx_add is_opaque (TraitImplId trait_impl.def_id) name ctx
+  ctx_add (TraitImplId trait_impl.def_id) name ctx
 
 (** Small helper.
 
@@ -4446,8 +4399,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (decl : trait_decl) : unit =
   (* Retrieve the trait name *)
-  let with_opaque_pre = false in
-  let decl_name = ctx_get_trait_decl with_opaque_pre decl.def_id ctx in
+  let decl_name = ctx_get_trait_decl decl.def_id ctx in
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
@@ -4592,7 +4544,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
       if use_forall then F.pp_print_string fmt ",";
       (* Extract the function call *)
       F.pp_print_space fmt ();
-      let id = ctx_get_local_function false f.def_id None f.back_id ctx in
+      let id = ctx_get_local_function f.def_id None f.back_id ctx in
       F.pp_print_string fmt id;
       let all_generics =
         let i_tys, i_cgs, i_tcs = impl_generics in
@@ -4613,8 +4565,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     (impl : trait_impl) : unit =
   log#ldebug (lazy ("extract_trait_impl: " ^ Names.name_to_string impl.name));
   (* Retrieve the impl name *)
-  let with_opaque_pre = false in
-  let impl_name = ctx_get_trait_impl with_opaque_pre impl.def_id ctx in
+  let impl_name = ctx_get_trait_impl impl.def_id ctx in
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
@@ -4690,7 +4641,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
       let item_name = ctx_get_trait_const trait_decl_id name ctx in
       let ty () =
         F.pp_print_space fmt ();
-        F.pp_print_string fmt (ctx_get_global false id ctx)
+        F.pp_print_string fmt (ctx_get_global id ctx)
       in
 
       extract_trait_impl_item ctx fmt item_name ty)
@@ -4776,12 +4727,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt "assert_norm";
         F.pp_print_space fmt ();
         F.pp_print_string fmt "(";
-        (* Note that if the function is opaque, the unit test will fail
-           because the normalizer will get stuck *)
-        let with_opaque_pre = ctx.use_opaque_pre in
         let fun_name =
-          ctx_get_local_function with_opaque_pre def.def_id def.loop_id
-            def.back_id ctx
+          ctx_get_local_function def.def_id def.loop_id def.back_id ctx
         in
         F.pp_print_string fmt fun_name;
         if sg.inputs <> [] then (
@@ -4796,12 +4743,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt "Check";
         F.pp_print_space fmt ();
         F.pp_print_string fmt "(";
-        (* Note that if the function is opaque, the unit test will fail
-           because the normalizer will get stuck *)
-        let with_opaque_pre = ctx.use_opaque_pre in
         let fun_name =
-          ctx_get_local_function with_opaque_pre def.def_id def.loop_id
-            def.back_id ctx
+          ctx_get_local_function def.def_id def.loop_id def.back_id ctx
         in
         F.pp_print_string fmt fun_name;
         if sg.inputs <> [] then (
@@ -4813,12 +4756,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt "#assert";
         F.pp_print_space fmt ();
         F.pp_print_string fmt "(";
-        (* Note that if the function is opaque, the unit test will fail
-           because the normalizer will get stuck *)
-        let with_opaque_pre = ctx.use_opaque_pre in
         let fun_name =
-          ctx_get_local_function with_opaque_pre def.def_id def.loop_id
-            def.back_id ctx
+          ctx_get_local_function def.def_id def.loop_id def.back_id ctx
         in
         F.pp_print_string fmt fun_name;
         if sg.inputs <> [] then (
@@ -4832,12 +4771,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
     | HOL4 ->
         F.pp_print_string fmt "val _ = assert_return (";
         F.pp_print_string fmt "“";
-        (* Note that if the function is opaque, the unit test will fail
-           because the normalizer will get stuck *)
-        let with_opaque_pre = ctx.use_opaque_pre in
         let fun_name =
-          ctx_get_local_function with_opaque_pre def.def_id def.loop_id
-            def.back_id ctx
+          ctx_get_local_function def.def_id def.loop_id def.back_id ctx
         in
         F.pp_print_string fmt fun_name;
         if sg.inputs <> [] then (
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 3ff299f2..f26beeb6 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -251,37 +251,6 @@ type formatter = {
   trait_type_name : trait_decl -> string -> string;
   trait_method_name : trait_decl -> string -> string;
   trait_type_clause_name : trait_decl -> string -> trait_clause -> string;
-  opaque_pre : unit -> string;
-      (** TODO: obsolete, remove.
-
-          The prefix to use for opaque definitions.
-
-          We need this because for some backends like Lean and Coq, we group
-          opaque definitions in module signatures, meaning that using those
-          definitions requires to prefix them with a module parameter name (such
-          as "opaque_defs.").
-
-          For instance, if we have an opaque function [f : int -> int], which
-          is used by the non-opaque function [g], we would generate (in Coq):
-          {[
-            (* The module signature declaring the opaque definitions *)
-            module type OpaqueDefs = {
-              f_fwd : int -> int
-              ... (* Other definitions *)
-            }
-
-            (* The definitions generated for the non-opaque definitions *)
-            module Funs (opaque: OpaqueDefs) = {
-              let g ... =
-                ...
-                opaque_defs.f_fwd
-                ...
-            }
-          ]}
-
-          Upon using [f] in [g], we don't directly use the the name "f_fwd",
-          but prefix it with the "opaque_defs." identifier.
-       *)
   var_basename : StringSet.t -> string option -> ty -> string;
       (** Generates a variable basename.
 
@@ -498,20 +467,6 @@ type names_map = {
           precisely which identifiers are mapped to the same name...
        *)
   names_set : StringSet.t;
-  opaque_ids : IdSet.t;
-      (** TODO: this is obsolete. Remove.
-
-          The set of opaque definitions.
-
-          See {!formatter.opaque_pre} for detailed explanations about why
-          we need to know which definitions are opaque to compute names.
-
-          Also note that the opaque ids don't contain the ids of the assumed
-          definitions. In practice, assumed definitions are opaque_defs. However, they
-          are not grouped in the opaque module, meaning we never need to
-          prefix them (with, say, "opaque_defs."): we thus consider them as non-opaque
-          with regards to the names map.
-       *)
 }
 
 let empty_names_map : names_map =
@@ -519,7 +474,6 @@ let empty_names_map : names_map =
     id_to_name = IdMap.empty;
     name_to_id = StringMap.empty;
     names_set = StringSet.empty;
-    opaque_ids = IdSet.empty;
   }
 
 (** Small helper to report name collision *)
@@ -547,8 +501,8 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
       (* There is a clash: print a nice debugging message for the user *)
       report_name_collision id_to_string clash id name
 
-let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id)
-    (name : string) (nm : names_map) : names_map =
+let names_map_add (id_to_string : id -> string) (id : id) (name : string)
+    (nm : names_map) : names_map =
   (* Check if there is a clash *)
   names_map_check_collision id_to_string id name nm;
   (* Sanity check *)
@@ -564,32 +518,24 @@ let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id)
   let id_to_name = IdMap.add id name nm.id_to_name in
   let name_to_id = StringMap.add name id nm.name_to_id in
   let names_set = StringSet.add name nm.names_set in
-  let opaque_ids =
-    if is_opaque then IdSet.add id nm.opaque_ids else nm.opaque_ids
-  in
-  { id_to_name; name_to_id; names_set; opaque_ids }
+  { id_to_name; name_to_id; names_set }
 
 let names_map_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
     (name : string) (nm : names_map) : names_map =
-  let is_opaque = false in
-  names_map_add id_to_string is_opaque (TypeId (Assumed id)) name nm
+  names_map_add id_to_string (TypeId (Assumed id)) name nm
 
 let names_map_add_assumed_struct (id_to_string : id -> string) (id : assumed_ty)
     (name : string) (nm : names_map) : names_map =
-  let is_opaque = false in
-  names_map_add id_to_string is_opaque (StructId (Assumed id)) name nm
+  names_map_add id_to_string (StructId (Assumed id)) name nm
 
 let names_map_add_assumed_variant (id_to_string : id -> string)
     (id : assumed_ty) (variant_id : VariantId.id) (name : string)
     (nm : names_map) : names_map =
-  let is_opaque = false in
-  names_map_add id_to_string is_opaque
-    (VariantId (Assumed id, variant_id))
-    name nm
+  names_map_add id_to_string (VariantId (Assumed id, variant_id)) name nm
 
-let names_map_add_function (id_to_string : id -> string) (is_opaque : bool)
-    (fid : fun_id) (name : string) (nm : names_map) : names_map =
-  names_map_add id_to_string is_opaque (FunId fid) name nm
+let names_map_add_function (id_to_string : id -> string) (fid : fun_id)
+    (name : string) (nm : names_map) : names_map =
+  names_map_add id_to_string (FunId fid) name nm
 
 (** The unsafe names map stores mappings from identifiers to names which might
     collide. For some backends and some names, it might be acceptable to have
@@ -667,14 +613,6 @@ type extraction_ctx = {
   fmt : formatter;
   indent_incr : int;
       (** The indent increment we insert whenever we need to indent more *)
-  use_opaque_pre : bool;
-      (** Do we use the "opaque_defs." prefix for the opaque definitions?
-
-          Opaque function definitions might refer opaque types: if we are in the
-          opaque module, we musn't use the "opaque_defs." prefix, otherwise we
-          use it.
-          Also see {!names_map.opaque_ids}.
-       *)
   use_dep_ite : bool;
       (** For Lean: do we use dependent-if then else expressions?
 
@@ -884,8 +822,7 @@ let allow_collisions (id : id) : bool =
       !Config.record_fields_short_names
   | _ -> false
 
-let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
-    : extraction_ctx =
+let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
   (* The id_to_string function to print nice debugging messages if there are
    * collisions *)
   let id_to_string (id : id) : string = id_to_string id ctx in
@@ -902,7 +839,6 @@ let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
      others (ex.: fields and keywords).
   *)
   if allow_collisions id then (
-    assert (not is_opaque);
     (* Check with the ids which are considered to be strict on collisions *)
     names_map_check_collision id_to_string id name ctx.strict_names_map;
     {
@@ -916,16 +852,13 @@ let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
     *)
     let strict_names_map =
       if strict_collisions id then
-        names_map_add id_to_string is_opaque id name ctx.strict_names_map
+        names_map_add id_to_string id name ctx.strict_names_map
       else ctx.strict_names_map
     in
-    let names_map =
-      names_map_add id_to_string is_opaque id name ctx.names_map
-    in
+    let names_map = names_map_add id_to_string id name ctx.names_map in
     { ctx with strict_names_map; names_map }
 
-(** [with_opaque_pre]: if [true] and the definition is opaque, add the opaque prefix *)
-let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
+let ctx_get (id : id) (ctx : extraction_ctx) : string =
   (* We do not use the same name map if we allow/disallow collisions *)
   let map_to_string (m : string IdMap.t) : string =
     "[\n"
@@ -951,9 +884,7 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
   else
     let m = ctx.names_map.id_to_name in
     match IdMap.find_opt id m with
-    | Some s ->
-        let is_opaque = IdSet.mem id ctx.names_map.opaque_ids in
-        if with_opaque_pre && is_opaque then ctx.fmt.opaque_pre () ^ s else s
+    | Some s -> s
     | None ->
         let err =
           "Could not find: " ^ id_to_string id ctx ^ "\nNames map:\n"
@@ -963,53 +894,38 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
         if !Config.extract_fail_hard then raise (Failure err)
         else "(ERROR: \"" ^ id_to_string id ctx ^ "\")"
 
-let ctx_get_global (with_opaque_pre : bool) (id : A.GlobalDeclId.id)
-    (ctx : extraction_ctx) : string =
-  ctx_get with_opaque_pre (GlobalId id) ctx
+let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
+  ctx_get (GlobalId id) ctx
 
-let ctx_get_function (with_opaque_pre : bool) (id : fun_id)
-    (ctx : extraction_ctx) : string =
-  ctx_get with_opaque_pre (FunId id) ctx
+let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string =
+  ctx_get (FunId id) ctx
 
-let ctx_get_local_function (with_opaque_pre : bool) (id : A.FunDeclId.id)
-    (lp : LoopId.id option) (rg : RegionGroupId.id option)
-    (ctx : extraction_ctx) : string =
-  ctx_get_function with_opaque_pre (FromLlbc (FunId (Regular id), lp, rg)) ctx
+let ctx_get_local_function (id : A.FunDeclId.id) (lp : LoopId.id option)
+    (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string =
+  ctx_get_function (FromLlbc (FunId (Regular id), lp, rg)) ctx
 
-let ctx_get_type (with_opaque_pre : bool) (id : type_id) (ctx : extraction_ctx)
-    : string =
+let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string =
   assert (id <> Tuple);
-  ctx_get with_opaque_pre (TypeId id) ctx
+  ctx_get (TypeId id) ctx
 
-let ctx_get_local_type (with_opaque_pre : bool) (id : TypeDeclId.id)
-    (ctx : extraction_ctx) : string =
-  ctx_get_type with_opaque_pre (AdtId id) ctx
+let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string =
+  ctx_get_type (AdtId id) ctx
 
 let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string =
-  (* In practice, the assumed types are opaque. However, assumed types
-     are never grouped in the opaque module, meaning we never need to
-     prefix them: we thus consider them as non-opaque with regards to the
-     names map.
-  *)
-  let is_opaque = false in
-  ctx_get_type is_opaque (Assumed id) ctx
+  ctx_get_type (Assumed id) ctx
 
 let ctx_get_trait_self_clause (ctx : extraction_ctx) : string =
-  let with_opaque_pre = false in
-  ctx_get with_opaque_pre TraitSelfClauseId ctx
+  ctx_get TraitSelfClauseId ctx
 
-let ctx_get_trait_decl (with_opaque_pre : bool) (id : trait_decl_id)
-    (ctx : extraction_ctx) : string =
-  ctx_get with_opaque_pre (TraitDeclId id) ctx
+let ctx_get_trait_decl (id : trait_decl_id) (ctx : extraction_ctx) : string =
+  ctx_get (TraitDeclId id) ctx
 
-let ctx_get_trait_impl (with_opaque_pre : bool) (id : trait_impl_id)
-    (ctx : extraction_ctx) : string =
-  ctx_get with_opaque_pre (TraitImplId id) ctx
+let ctx_get_trait_impl (id : trait_impl_id) (ctx : extraction_ctx) : string =
+  ctx_get (TraitImplId id) ctx
 
 let ctx_get_trait_item (id : trait_decl_id) (item_name : string)
     (ctx : extraction_ctx) : string =
-  let is_opaque = false in
-  ctx_get is_opaque (TraitItemId (id, item_name)) ctx
+  ctx_get (TraitItemId (id, item_name)) ctx
 
 let ctx_get_trait_const (id : trait_decl_id) (item_name : string)
     (ctx : extraction_ctx) : string =
@@ -1021,83 +937,69 @@ let ctx_get_trait_type (id : trait_decl_id) (item_name : string)
 
 let ctx_get_trait_method (id : trait_decl_id) (item_name : string)
     (rg_id : T.RegionGroupId.id option) (ctx : extraction_ctx) : string =
-  let with_opaque_pre = false in
-  ctx_get with_opaque_pre (TraitMethodId (id, item_name, rg_id)) ctx
+  ctx_get (TraitMethodId (id, item_name, rg_id)) ctx
 
 let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id)
     (ctx : extraction_ctx) : string =
-  let with_opaque_pre = false in
-  ctx_get with_opaque_pre (TraitParentClauseId (id, clause)) ctx
+  ctx_get (TraitParentClauseId (id, clause)) ctx
 
 let ctx_get_trait_item_clause (id : trait_decl_id) (item : string)
     (clause : trait_clause_id) (ctx : extraction_ctx) : string =
-  let with_opaque_pre = false in
-  ctx_get with_opaque_pre (TraitItemClauseId (id, item, clause)) ctx
+  ctx_get (TraitItemClauseId (id, item, clause)) ctx
 
 let ctx_get_var (id : VarId.id) (ctx : extraction_ctx) : string =
-  let is_opaque = false in
-  ctx_get is_opaque (VarId id) ctx
+  ctx_get (VarId id) ctx
 
 let ctx_get_type_var (id : TypeVarId.id) (ctx : extraction_ctx) : string =
-  let is_opaque = false in
-  ctx_get is_opaque (TypeVarId id) ctx
+  ctx_get (TypeVarId id) ctx
 
 let ctx_get_const_generic_var (id : ConstGenericVarId.id) (ctx : extraction_ctx)
     : string =
-  let is_opaque = false in
-  ctx_get is_opaque (ConstGenericVarId id) ctx
+  ctx_get (ConstGenericVarId id) ctx
 
 let ctx_get_local_trait_clause (id : TraitClauseId.id) (ctx : extraction_ctx) :
     string =
-  let is_opaque = false in
-  ctx_get is_opaque (LocalTraitClauseId id) ctx
+  ctx_get (LocalTraitClauseId id) ctx
 
 let ctx_get_field (type_id : type_id) (field_id : FieldId.id)
     (ctx : extraction_ctx) : string =
-  let is_opaque = false in
-  ctx_get is_opaque (FieldId (type_id, field_id)) ctx
+  ctx_get (FieldId (type_id, field_id)) ctx
 
-let ctx_get_struct (with_opaque_pre : bool) (def_id : type_id)
-    (ctx : extraction_ctx) : string =
-  ctx_get with_opaque_pre (StructId def_id) ctx
+let ctx_get_struct (def_id : type_id) (ctx : extraction_ctx) : string =
+  ctx_get (StructId def_id) ctx
 
 let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
     (ctx : extraction_ctx) : string =
-  let is_opaque = false in
-  ctx_get is_opaque (VariantId (def_id, variant_id)) ctx
+  ctx_get (VariantId (def_id, variant_id)) ctx
 
 let ctx_get_decreases_proof (def_id : A.FunDeclId.id)
     (loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
-  let is_opaque = false in
-  ctx_get is_opaque (DecreasesProofId (Regular def_id, loop_id)) ctx
+  ctx_get (DecreasesProofId (Regular def_id, loop_id)) ctx
 
 let ctx_get_termination_measure (def_id : A.FunDeclId.id)
     (loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
-  let is_opaque = false in
-  ctx_get is_opaque (TerminationMeasureId (Regular def_id, loop_id)) ctx
+  ctx_get (TerminationMeasureId (Regular def_id, loop_id)) ctx
 
 (** Generate a unique type variable name and add it to the context *)
 let ctx_add_type_var (basename : string) (id : TypeVarId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
-  let is_opaque = false in
   let name = ctx.fmt.type_var_basename ctx.names_map.names_set basename in
   let name =
     basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name
   in
-  let ctx = ctx_add is_opaque (TypeVarId id) name ctx in
+  let ctx = ctx_add (TypeVarId id) name ctx in
   (ctx, name)
 
 (** Generate a unique const generic variable name and add it to the context *)
 let ctx_add_const_generic_var (basename : string) (id : ConstGenericVarId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
-  let is_opaque = false in
   let name =
     ctx.fmt.const_generic_var_basename ctx.names_map.names_set basename
   in
   let name =
     basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name
   in
-  let ctx = ctx_add is_opaque (ConstGenericVarId id) name ctx in
+  let ctx = ctx_add (ConstGenericVarId id) name ctx in
   (ctx, name)
 
 (** See {!ctx_add_type_var} *)
@@ -1110,31 +1012,28 @@ let ctx_add_type_vars (vars : (string * TypeVarId.id) list)
 (** Generate a unique variable name and add it to the context *)
 let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) :
     extraction_ctx * string =
-  let is_opaque = false in
   let name =
     basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
   in
-  let ctx = ctx_add is_opaque (VarId id) name ctx in
+  let ctx = ctx_add (VarId id) name ctx in
   (ctx, name)
 
 (** Generate a unique variable name for the trait self clause and add it to the context *)
 let ctx_add_trait_self_clause (ctx : extraction_ctx) : extraction_ctx * string =
-  let is_opaque = false in
   let basename = ctx.fmt.trait_self_clause_basename in
   let name =
     basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
   in
-  let ctx = ctx_add is_opaque TraitSelfClauseId name ctx in
+  let ctx = ctx_add TraitSelfClauseId name ctx in
   (ctx, name)
 
 (** Generate a unique trait clause name and add it to the context *)
 let ctx_add_local_trait_clause (basename : string) (id : TraitClauseId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
-  let is_opaque = false in
   let name =
     basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
   in
-  let ctx = ctx_add is_opaque (LocalTraitClauseId id) name ctx in
+  let ctx = ctx_add (LocalTraitClauseId id) name ctx in
   (ctx, name)
 
 (** See {!ctx_add_var} *)
@@ -1182,30 +1081,23 @@ let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) :
 
 let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
-  let is_opaque = false in
   let name =
     ctx.fmt.decreases_proof_name def.def_id def.basename def.num_loops
       def.loop_id
   in
-  ctx_add is_opaque
-    (DecreasesProofId (Regular def.def_id, def.loop_id))
-    name ctx
+  ctx_add (DecreasesProofId (Regular def.def_id, def.loop_id)) name ctx
 
 let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
-  let is_opaque = false in
   let name =
     ctx.fmt.termination_measure_name def.def_id def.basename def.num_loops
       def.loop_id
   in
-  ctx_add is_opaque
-    (TerminationMeasureId (Regular def.def_id, def.loop_id))
-    name ctx
+  ctx_add (TerminationMeasureId (Regular def.def_id, def.loop_id)) name ctx
 
 let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   (* TODO: update once the body id can be an option *)
-  let is_opaque = false in
   let decl = GlobalId def.def_id in
 
   (* Check if the global corresponds to an assumed global that we should map
@@ -1215,13 +1107,13 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
   match SimpleNameMap.find_opt sname builtin_globals_map with
   | Some name ->
       (* Yes: register the custom binding *)
-      ctx_add is_opaque decl name ctx
+      ctx_add decl name ctx
   | None ->
       (* Not the case: "standard" registration *)
       let name = ctx.fmt.global_name def.name in
       let body = FunId (FromLlbc (FunId (Regular def.body_id), None, None)) in
-      let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in
-      let ctx = ctx_add is_opaque body (name ^ "_body") ctx in
+      let ctx = ctx_add decl (name ^ "_c") ctx in
+      let ctx = ctx_add body (name ^ "_body") ctx in
       ctx
 
 let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
@@ -1259,11 +1151,10 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
   let def_id = def.def_id in
   let { keep_fwd; fwd = _; backs } = trans_group in
   let num_backs = List.length backs in
-  let is_opaque = def.body = None in
   (* Add the function name *)
   let def_name = ctx_compute_fun_name trans_group def ctx in
   let fun_id = (Pure.FunId (Regular def_id), def.loop_id, def.back_id) in
-  let ctx = ctx_add is_opaque (FunId (FromLlbc fun_id)) def_name ctx in
+  let ctx = ctx_add (FunId (FromLlbc fun_id)) def_name ctx in
   (* Add the name info *)
   {
     ctx with
@@ -1296,12 +1187,11 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
   let name_to_id =
     StringMap.of_list (List.map (fun x -> (x, UnknownId)) keywords)
   in
-  let opaque_ids = IdSet.empty in
   (* We fist initialize [id_to_name] as empty, because the id of a keyword is [UnknownId].
    * Also note that we don't need this mapping for keywords: we insert keywords only
    * to check collisions. *)
   let id_to_name = IdMap.empty in
-  let nm = { id_to_name; name_to_id; names_set; opaque_ids } in
+  let nm = { id_to_name; name_to_id; names_set } in
   (* For debugging - we are creating bindings for assumed types and functions, so
    * it is ok if we simply use the "show" function (those aren't simply identified
    * by numbers) *)
@@ -1338,15 +1228,8 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
     @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
   in
   let nm =
-    (* In practice, the assumed function are opaque. However, assumed functions
-       are never grouped in the opaque module, meaning we never need to
-       prefix them: we thus consider them as non-opaque with regards to the
-       names map.
-    *)
-    let is_opaque = false in
     List.fold_left
-      (fun nm (fid, name) ->
-        names_map_add_function id_to_string is_opaque fid name nm)
+      (fun nm (fid, name) -> names_map_add_function id_to_string fid name nm)
       nm assumed_functions
   in
   (* Return *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 74a8537f..b3269aa2 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -851,37 +851,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
   if config.extract_state_type && config.extract_fun_decls then
     export_state_type ();
 
-  (* Obsolete: (TODO: remove) For Lean we parameterize the entire development by a section
-     variable called opaque_defs, of type OpaqueDefs. The code below emits the type
-     definition for OpaqueDefs, which is a structure, in which each field is one of the
-     functions marked as Opaque. We emit the `structure ...` bit here, then rely on
-     `extract_fun_decl` to be aware of this, and skip the keyword (e.g. "axiom" or "val")
-     so as to generate valid syntax for records.
-
-     We also generate such a structure only if there actually are opaque definitions. *)
-  let wrap_in_sig =
-    config.extract_opaque && config.extract_fun_decls
-    && !Config.wrap_opaque_in_sig
-    &&
-    let _, opaque_funs = crate_has_opaque_decls ctx true in
-    opaque_funs
-  in
-  if wrap_in_sig then (
-    (* We change the name of the structure depending on whether we *only*
-       extract opaque definitions, or if we extract all definitions *)
-    let struct_name =
-      if config.extract_transparent then "Definitions" else "OpaqueDefs"
-    in
-    Format.pp_print_break fmt 0 0;
-    Format.pp_open_vbox fmt ctx.indent_incr;
-    Format.pp_print_string fmt ("structure " ^ struct_name ^ " where");
-    Format.pp_print_break fmt 0 0);
   List.iter export_decl_group ctx.crate.declarations;
 
   if config.extract_state_type && not config.extract_fun_decls then
-    export_state_type ();
-
-  if wrap_in_sig then Format.pp_close_box fmt ()
+    export_state_type ()
 
 type extract_file_info = {
   filename : string;
@@ -1029,10 +1002,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         (fun (id, _) -> strict_collisions id)
         (IdMap.bindings names_map.id_to_name)
     in
-    let is_opaque = false in
     List.fold_left
       (* id_to_string: we shouldn't need to use it *)
-        (fun m (id, n) -> names_map_add show_id is_opaque id n m)
+        (fun m (id, n) -> names_map_add show_id id n m)
       empty_names_map ids
   in
 
@@ -1093,7 +1065,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       strict_names_map;
       fmt;
       indent_incr = 2;
-      use_opaque_pre = !Config.split_files;
       use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
       fun_name_info = PureUtils.RegularFunIdMap.empty;
       trait_decl_id = None (* None by default *);
@@ -1389,7 +1360,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
              interface = true;
            }
          in
-         let ctx = { ctx with use_opaque_pre = false } in
          let file_info =
            {
              filename = opaque_filename;
-- 
cgit v1.3.1


From 9df1d191cfaf929b755e9d26d55811531acd939d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 11:21:53 +0100
Subject: Fix a small issue in AssociatedTypes

---
 compiler/AssociatedTypes.ml |  2 +-
 compiler/Config.ml          |  6 +++---
 compiler/Driver.ml          |  8 +++++++-
 compiler/Extract.ml         |  4 ++--
 compiler/ExtractBase.ml     | 12 ++++++------
 compiler/ExtractTypes.ml    |  2 +-
 compiler/Logging.ml         |  2 +-
 7 files changed, 21 insertions(+), 15 deletions(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index e4015903..581e218c 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -451,7 +451,7 @@ and ctx_normalize_trait_instance_id :
       | None ->
           (* This is actually a local clause *)
           assert (trait_instance_id_is_local_clause inst_id);
-          (ParentClause (inst_id, decl_id, clause_id), None)
+          (ItemClause (inst_id, decl_id, item_name, clause_id), None)
       | Some impl ->
           (* We figure out the item clause by doing the following:
              {[
diff --git a/compiler/Config.ml b/compiler/Config.ml
index cd0903b6..8483c879 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -333,6 +333,6 @@ let parameterize_trait_types = ref false
  *)
 let type_check_pure_code = ref false
 
-(** Shall we fail hard if there is an issue at code-generation time?
-    We may not want in case outputting a code with holes helps debugging *)
-let extract_fail_hard = ref false
+(** Shall we fail hard if we encounter an issue, or should we attempt to go
+    as far as possible while leaving "holes" in the generated code? *)
+let fail_hard = ref true
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index b660b5a5..14668632 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -41,7 +41,7 @@ let _ =
   pure_utils_log#set_level EL.Info;
   symbolic_to_pure_log#set_level EL.Info;
   pure_micro_passes_log#set_level EL.Info;
-  pure_to_extract_log#set_level EL.Info;
+  extract_log#set_level EL.Info;
   translate_log#set_level EL.Info;
   scc_log#set_level EL.Info;
   reorder_decls_log#set_level EL.Info
@@ -66,6 +66,9 @@ let () =
   (* Read the command line arguments *)
   let dest_dir = ref "" in
 
+  (* Print the imported llbc *)
+  let print_llbc = ref false in
+
   let spec =
     [
       ( "-backend",
@@ -118,6 +121,8 @@ let () =
       ( "-lean-default-lakefile",
         Arg.Clear lean_gen_lakefile,
         " Generate a default lakefile.lean (Lean only)" );
+      ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC");
+      ("-k", Arg.Clear fail_hard, " Do not fail hard in case of error");
     ]
   in
 
@@ -131,6 +136,7 @@ let () =
   in
 
   if !extract_template_decreases_clauses then extract_decreases_clauses := true;
+  if !print_llbc then main_log#set_level EL.Debug;
 
   (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *)
   assert (!extract_decreases_clauses || not !extract_template_decreases_clauses);
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 8ad8a18d..b8cb38bb 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -472,7 +472,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
       | Error (types, err) ->
           extract_generic_args ctx fmt TypeDeclId.Set.empty
             { generics with types };
-          if !Config.extract_fail_hard then raise (Failure err)
+          if !Config.fail_hard then raise (Failure err)
           else
             F.pp_print_string fmt
               "(\"ERROR: ill-formed builtin: invalid number of filtering \
@@ -1992,7 +1992,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
                         trans_fun.back_id
                   in
                   log#serror err;
-                  if !Config.extract_fail_hard then raise (Failure err)
+                  if !Config.fail_hard then raise (Failure err)
                   else (trans_fun.back_id, "%ERROR_BUILTIN_NAME_NOT_FOUND%")
             in
             let rg_with_name_list = List.map find trans_funs in
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 8ddb2ec6..55b1bca3 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -8,7 +8,7 @@ module F = Format
 open ExtractBuiltin
 
 (** The local logger *)
-let log = L.pure_to_extract_log
+let log = L.extract_log
 
 type region_group_info = {
   id : RegionGroupId.id;
@@ -488,7 +488,7 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
   in
   log#serror err;
   (* If we fail hard on errors, raise an exception *)
-  if !Config.extract_fail_hard then raise (Failure err)
+  if !Config.fail_hard then raise (Failure err)
 
 let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
   StringMap.find_opt name nm.name_to_id
@@ -522,7 +522,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
     in
     log#serror err;
     (* If we fail hard on errors, raise an exception *)
-    if !Config.extract_fail_hard then raise (Failure err));
+    if !Config.fail_hard then raise (Failure err));
   (* Insert *)
   names_map_add_unchecked id name nm
 
@@ -691,7 +691,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
             | FunId (Assumed aid) -> A.show_assumed_fun_id aid
             | TraitMethod (trait_ref, method_name, _) ->
                 (* Shouldn't happen *)
-                if !Config.extract_fail_hard then raise (Failure "Unexpected")
+                if !Config.fail_hard then raise (Failure "Unexpected")
                 else
                   "Trait method: decl: "
                   ^ TraitDeclId.to_string trait_ref.trait_decl_ref.trait_decl_id
@@ -903,7 +903,7 @@ let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) :
           ^ map_to_string m
         in
         log#serror err;
-        if !Config.extract_fail_hard then raise (Failure err)
+        if !Config.fail_hard then raise (Failure err)
         else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)")
   else
     let m = nm.names_map.id_to_name in
@@ -915,7 +915,7 @@ let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) :
           ^ map_to_string m
         in
         log#serror err;
-        if !Config.extract_fail_hard then raise (Failure err)
+        if !Config.fail_hard then raise (Failure err)
         else "(ERROR: \"" ^ id_to_string id ^ "\")"
 
 let ctx_get (id : id) (ctx : extraction_ctx) : string =
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 7bd02381..699a0e96 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1374,7 +1374,7 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
   | Self ->
       (* This has a specific treatment depending on the item we're extracting
          (associated type, etc.). We should have caught this elsewhere. *)
-      if !Config.extract_fail_hard then
+      if !Config.fail_hard then
         raise (Failure "Unexpected occurrence of `Self`")
       else F.pp_print_string fmt "ERROR(\"Unexpected Self\")"
   | TraitImpl id ->
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 59abbfc7..721655b8 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -22,7 +22,7 @@ let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure"
 let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses"
 
 (** Logger for ExtractBase *)
-let pure_to_extract_log = L.get_logger "MainLogger.ExtractBase"
+let extract_log = L.get_logger "MainLogger.ExtractBase"
 
 (** Logger for Interpreter *)
 let interpreter_log = L.get_logger "MainLogger.Interpreter"
-- 
cgit v1.3.1


From c57dec640d4e12c3dc66969d626bbbca2eb733fd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 11:43:47 +0100
Subject: Modify some options and update the Makefile

---
 Makefile                     |  26 +-
 compiler/Config.ml           |   4 +-
 compiler/Driver.ml           |  14 +-
 tests/fstar/misc/Loops.fst   | 784 +++++++++++++++++++++++++++++++++++++++++++
 tests/lean/Array.lean        | 436 +++++++++++++++++++++++-
 tests/lean/Loops.lean        | 630 +++++++++++++++++++++++++++++++++-
 tests/lean/Loops/Funs.lean   | 625 ----------------------------------
 tests/lean/Loops/Types.lean  |  13 -
 tests/lean/Traits.lean       | 411 ++++++++++++++++++++++-
 tests/lean/Traits/Funs.lean  | 275 ---------------
 tests/lean/Traits/Types.lean | 144 --------
 11 files changed, 2280 insertions(+), 1082 deletions(-)
 create mode 100644 tests/fstar/misc/Loops.fst
 delete mode 100644 tests/lean/Loops/Funs.lean
 delete mode 100644 tests/lean/Loops/Types.lean
 delete mode 100644 tests/lean/Traits/Funs.lean
 delete mode 100644 tests/lean/Traits/Types.lean

(limited to 'compiler/Config.ml')

diff --git a/Makefile b/Makefile
index bdabe878..19992442 100644
--- a/Makefile
+++ b/Makefile
@@ -115,7 +115,7 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA
 
 # Add specific options to some tests
 test-no_nested_borrows test-paper: \
-	OPTIONS += -test-trans-units -no-split-files -no-state
+	OPTIONS += -test-trans-units
 test-no_nested_borrows test-paper: SUBDIR := misc
 tfstar-no_nested_borrows tfstar-paper:
 tlean-no_nested_borrows: SUBDIR :=
@@ -123,7 +123,7 @@ tlean-paper: SUBDIR :=
 thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
 thol4-paper: SUBDIR := misc-paper
 
-test-array: OPTIONS += -no-state
+test-array: OPTIONS +=
 test-array: SUBDIR := array
 tfstar-array: OPTIONS += -decreases-clauses -template-clauses
 tcoq-array: OPTIONS += -use-fuel
@@ -131,7 +131,7 @@ tlean-array: SUBDIR :=
 tlean-array: OPTIONS +=
 thol4-array: OPTIONS +=
 
-test-traits: OPTIONS += -no-state
+test-traits: OPTIONS +=
 test-traits: SUBDIR := traits
 tfstar-traits: OPTIONS += -decreases-clauses -template-clauses
 tcoq-traits: OPTIONS += -use-fuel
@@ -147,15 +147,15 @@ thol4-array:
 thol4-traits:
 	echo "Ignoring the traits test for HOL4"
 
-test-loops: OPTIONS += -no-state
+test-loops: OPTIONS +=
 test-loops: SUBDIR := misc
-tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
-tcoq-loops: OPTIONS += -use-fuel -no-split-files
+tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files
+tcoq-loops: OPTIONS += -use-fuel
 tlean-loops: SUBDIR :=
 thol4-loops: SUBDIR := misc-loops
 
 # TODO: reactivate -test-trans-units
-test-hashmap: OPTIONS += -no-state
+test-hashmap: OPTIONS += -split-files
 test-hashmap: SUBDIR := hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap: OPTIONS += -use-fuel
@@ -164,14 +164,14 @@ tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hash
 thol4-hashmap: OPTIONS +=
 
 # TODO: reactivate -test-trans-units
-test-hashmap_main: OPTIONS +=
+test-hashmap_main: OPTIONS += -state -split-files
 test-hashmap_main: SUBDIR := hashmap_on_disk
 tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap_main: OPTIONS += -use-fuel
 tlean-hashmap_main: SUBDIR :=
 thol4-hashmap_main: OPTIONS +=
 
-testp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state
+testp-polonius_list: OPTIONS += -test-trans-units
 testp-polonius_list: SUBDIR := misc
 tfstarp-polonius_list: OPTIONS +=
 tcoqp-polonius_list: OPTIONS +=
@@ -180,7 +180,7 @@ tleanp-polonius_list: OPTIONS +=
 thol4p-polonius_list: SUBDIR := misc-polonius_list
 thol4p-polonius_list: OPTIONS +=
 
-test-constants: OPTIONS += -test-trans-units -no-split-files -no-state
+test-constants: OPTIONS += -test-trans-units
 test-constants: SUBDIR := misc
 tfstar-constants: OPTIONS +=
 tcoq-constants: OPTIONS +=
@@ -189,7 +189,7 @@ tlean-constants: OPTIONS +=
 thol4-constants: SUBDIR := misc-constants
 thol4-constants: OPTIONS +=
 
-test-external: OPTIONS += -test-trans-units
+test-external: OPTIONS += -test-trans-units -state -split-files
 test-external: SUBDIR := misc
 tfstar-external: OPTIONS +=
 tcoq-external: OPTIONS +=
@@ -199,7 +199,7 @@ thol4-external: SUBDIR := misc-external
 thol4-external: OPTIONS +=
 
 BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
-testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units
+testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
 testp-betree_main: SUBDIR:=betree
 tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 tcoqp-betree_main: OPTIONS += -use-fuel
@@ -211,7 +211,7 @@ thol4-betree_main: OPTIONS +=
 # This generates very ugly code, but is good to test the translation.
 .PHONY: ctest-testp-betree_main
 ctest-testp-betree_main: testp-betree_main
-ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units
+ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files
 ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 ctest-testp-betree_main: BACKEND_SUBDIR := "fstar"
 ctest-testp-betree_main: SUBDIR:=betree_back_stateful
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 8483c879..a487f9e2 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -124,7 +124,7 @@ let always_deconstruct_adts_with_matches = ref false
 (** Controls whether we need to use a state to model the external world
     (I/O, for instance).
  *)
-let use_state = ref true
+let use_state = ref false
 
 (** Controls whether we use fuel to control termination.
  *)
@@ -160,7 +160,7 @@ let backward_no_state_update = ref false
     files for the types, clauses and functions, or if we group them in
     one file.
  *)
-let split_files = ref true
+let split_files = ref false
 
 (** Generate the library entry point, if the crate is split between different files.
 
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 14668632..128ae890 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -93,9 +93,9 @@ let () =
         Arg.Set extract_decreases_clauses,
         " Use decreases clauses/termination measures for the recursive \
          definitions" );
-      ( "-no-state",
-        Arg.Clear use_state,
-        " Do not use state-error monads, simply use error monads" );
+      ( "-state",
+        Arg.Set use_state,
+        " Use a *state*-error monads, instead of an error monads" );
       ( "-use-fuel",
         Arg.Set use_fuel,
         " Use a fuel parameter to control divergence" );
@@ -106,10 +106,10 @@ let () =
         Arg.Set extract_template_decreases_clauses,
         " Generate templates for the required decreases clauses/termination \
          measures, in a dedicated file. Implies -decreases-clauses" );
-      ( "-no-split-files",
-        Arg.Clear split_files,
-        " Do not split the definitions between different files for types, \
-         functions, etc." );
+      ( "-split-files",
+        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 \
diff --git a/tests/fstar/misc/Loops.fst b/tests/fstar/misc/Loops.fst
new file mode 100644
index 00000000..823acdd4
--- /dev/null
+++ b/tests/fstar/misc/Loops.fst
@@ -0,0 +1,784 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops] *)
+module Loops
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::sum]: decreases clause *)
+unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
+
+(** [loops::sum]: loop 0: forward function *)
+let rec sum_loop
+  (max : u32) (i : u32) (s : u32) :
+  Tot (result u32) (decreases (sum_loop_decreases max i s))
+  =
+  if i < max
+  then let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop max i0 s0
+  else u32_mul s 2
+
+(** [loops::sum]: forward function *)
+let sum (max : u32) : result u32 =
+  sum_loop max 0 0
+
+(** [loops::sum_with_mut_borrows]: decreases clause *)
+unfold
+let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat
+  =
+  admit ()
+
+(** [loops::sum_with_mut_borrows]: loop 0: forward function *)
+let rec sum_with_mut_borrows_loop
+  (max : u32) (mi : u32) (ms : u32) :
+  Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms))
+  =
+  if mi < max
+  then
+    let* ms0 = u32_add ms mi in
+    let* mi0 = u32_add mi 1 in
+    sum_with_mut_borrows_loop max mi0 ms0
+  else u32_mul ms 2
+
+(** [loops::sum_with_mut_borrows]: forward function *)
+let sum_with_mut_borrows (max : u32) : result u32 =
+  sum_with_mut_borrows_loop max 0 0
+
+(** [loops::sum_with_shared_borrows]: decreases clause *)
+unfold
+let sum_with_shared_borrows_loop_decreases (max : u32) (i : u32) (s : u32) :
+  nat =
+  admit ()
+
+(** [loops::sum_with_shared_borrows]: loop 0: forward function *)
+let rec sum_with_shared_borrows_loop
+  (max : u32) (i : u32) (s : u32) :
+  Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s))
+  =
+  if i < max
+  then
+    let* i0 = u32_add i 1 in
+    let* s0 = u32_add s i0 in
+    sum_with_shared_borrows_loop max i0 s0
+  else u32_mul s 2
+
+(** [loops::sum_with_shared_borrows]: forward function *)
+let sum_with_shared_borrows (max : u32) : result u32 =
+  sum_with_shared_borrows_loop max 0 0
+
+(** [loops::clear]: decreases clause *)
+unfold
+let clear_loop_decreases (v : alloc_vec_Vec u32) (i : usize) : nat = admit ()
+
+(** [loops::clear]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let rec clear_loop
+  (v : alloc_vec_Vec u32) (i : usize) :
+  Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i))
+  =
+  let i0 = alloc_vec_Vec_len u32 v in
+  if i < i0
+  then
+    let* i1 = usize_add i 1 in
+    let* v0 =
+      alloc_vec_Vec_index_mut_back u32 usize
+        (core_slice_index_usize_coresliceindexSliceIndexInst u32) v i 0 in
+    clear_loop v0 i1
+  else Return v
+
+(** [loops::clear]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) =
+  clear_loop v 0
+
+(** [loops::List] *)
+type list_t (t : Type0) =
+| List_Cons : t -> list_t t -> list_t t
+| List_Nil : list_t t
+
+(** [loops::list_mem]: decreases clause *)
+unfold let list_mem_loop_decreases (x : u32) (ls : list_t u32) : nat = admit ()
+
+(** [loops::list_mem]: loop 0: forward function *)
+let rec list_mem_loop
+  (x : u32) (ls : list_t u32) :
+  Tot (result bool) (decreases (list_mem_loop_decreases x ls))
+  =
+  begin match ls with
+  | List_Cons y tl -> if y = x then Return true else list_mem_loop x tl
+  | List_Nil -> Return false
+  end
+
+(** [loops::list_mem]: forward function *)
+let list_mem (x : u32) (ls : list_t u32) : result bool =
+  list_mem_loop x ls
+
+(** [loops::list_nth_mut_loop]: decreases clause *)
+unfold
+let list_nth_mut_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) :
+  nat =
+  admit ()
+
+(** [loops::list_nth_mut_loop]: loop 0: forward function *)
+let rec list_nth_mut_loop_loop
+  (t : Type0) (ls : list_t t) (i : u32) :
+  Tot (result t) (decreases (list_nth_mut_loop_loop_decreases t ls i))
+  =
+  begin match ls with
+  | List_Cons x tl ->
+    if i = 0
+    then Return x
+    else let* i0 = u32_sub i 1 in list_nth_mut_loop_loop t tl i0
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop]: forward function *)
+let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result t =
+  list_nth_mut_loop_loop t ls i
+
+(** [loops::list_nth_mut_loop]: loop 0: backward function 0 *)
+let rec list_nth_mut_loop_loop_back
+  (t : Type0) (ls : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t)) (decreases (list_nth_mut_loop_loop_decreases t ls i))
+  =
+  begin match ls with
+  | List_Cons x tl ->
+    if i = 0
+    then Return (List_Cons ret tl)
+    else
+      let* i0 = u32_sub i 1 in
+      let* tl0 = list_nth_mut_loop_loop_back t tl i0 ret in
+      Return (List_Cons x tl0)
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop]: backward function 0 *)
+let list_nth_mut_loop_back
+  (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
+  list_nth_mut_loop_loop_back t ls i ret
+
+(** [loops::list_nth_shared_loop]: decreases clause *)
+unfold
+let list_nth_shared_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) :
+  nat =
+  admit ()
+
+(** [loops::list_nth_shared_loop]: loop 0: forward function *)
+let rec list_nth_shared_loop_loop
+  (t : Type0) (ls : list_t t) (i : u32) :
+  Tot (result t) (decreases (list_nth_shared_loop_loop_decreases t ls i))
+  =
+  begin match ls with
+  | List_Cons x tl ->
+    if i = 0
+    then Return x
+    else let* i0 = u32_sub i 1 in list_nth_shared_loop_loop t tl i0
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_loop]: forward function *)
+let list_nth_shared_loop (t : Type0) (ls : list_t t) (i : u32) : result t =
+  list_nth_shared_loop_loop t ls i
+
+(** [loops::get_elem_mut]: decreases clause *)
+unfold
+let get_elem_mut_loop_decreases (x : usize) (ls : list_t usize) : nat =
+  admit ()
+
+(** [loops::get_elem_mut]: loop 0: forward function *)
+let rec get_elem_mut_loop
+  (x : usize) (ls : list_t usize) :
+  Tot (result usize) (decreases (get_elem_mut_loop_decreases x ls))
+  =
+  begin match ls with
+  | List_Cons y tl -> if y = x then Return y else get_elem_mut_loop x tl
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::get_elem_mut]: forward function *)
+let get_elem_mut
+  (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize =
+  let* l =
+    alloc_vec_Vec_index_mut (list_t usize) usize
+      (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize))
+      slots 0 in
+  get_elem_mut_loop x l
+
+(** [loops::get_elem_mut]: loop 0: backward function 0 *)
+let rec get_elem_mut_loop_back
+  (x : usize) (ls : list_t usize) (ret : usize) :
+  Tot (result (list_t usize)) (decreases (get_elem_mut_loop_decreases x ls))
+  =
+  begin match ls with
+  | List_Cons y tl ->
+    if y = x
+    then Return (List_Cons ret tl)
+    else let* tl0 = get_elem_mut_loop_back x tl ret in Return (List_Cons y tl0)
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::get_elem_mut]: backward function 0 *)
+let get_elem_mut_back
+  (slots : alloc_vec_Vec (list_t usize)) (x : usize) (ret : usize) :
+  result (alloc_vec_Vec (list_t usize))
+  =
+  let* l =
+    alloc_vec_Vec_index_mut (list_t usize) usize
+      (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize))
+      slots 0 in
+  let* l0 = get_elem_mut_loop_back x l ret in
+  alloc_vec_Vec_index_mut_back (list_t usize) usize
+    (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) slots
+    0 l0
+
+(** [loops::get_elem_shared]: decreases clause *)
+unfold
+let get_elem_shared_loop_decreases (x : usize) (ls : list_t usize) : nat =
+  admit ()
+
+(** [loops::get_elem_shared]: loop 0: forward function *)
+let rec get_elem_shared_loop
+  (x : usize) (ls : list_t usize) :
+  Tot (result usize) (decreases (get_elem_shared_loop_decreases x ls))
+  =
+  begin match ls with
+  | List_Cons y tl -> if y = x then Return y else get_elem_shared_loop x tl
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::get_elem_shared]: forward function *)
+let get_elem_shared
+  (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize =
+  let* l =
+    alloc_vec_Vec_index (list_t usize) usize
+      (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize))
+      slots 0 in
+  get_elem_shared_loop x l
+
+(** [loops::id_mut]: forward function *)
+let id_mut (t : Type0) (ls : list_t t) : result (list_t t) =
+  Return ls
+
+(** [loops::id_mut]: backward function 0 *)
+let id_mut_back
+  (t : Type0) (ls : list_t t) (ret : list_t t) : result (list_t t) =
+  Return ret
+
+(** [loops::id_shared]: forward function *)
+let id_shared (t : Type0) (ls : list_t t) : result (list_t t) =
+  Return ls
+
+(** [loops::list_nth_mut_loop_with_id]: decreases clause *)
+unfold
+let list_nth_mut_loop_with_id_loop_decreases (t : Type0) (i : u32)
+  (ls : list_t t) : nat =
+  admit ()
+
+(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *)
+let rec list_nth_mut_loop_with_id_loop
+  (t : Type0) (i : u32) (ls : list_t t) :
+  Tot (result t) (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls))
+  =
+  begin match ls with
+  | List_Cons x tl ->
+    if i = 0
+    then Return x
+    else let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop t i0 tl
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_with_id]: forward function *)
+let list_nth_mut_loop_with_id
+  (t : Type0) (ls : list_t t) (i : u32) : result t =
+  let* ls0 = id_mut t ls in list_nth_mut_loop_with_id_loop t i ls0
+
+(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *)
+let rec list_nth_mut_loop_with_id_loop_back
+  (t : Type0) (i : u32) (ls : list_t t) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls))
+  =
+  begin match ls with
+  | List_Cons x tl ->
+    if i = 0
+    then Return (List_Cons ret tl)
+    else
+      let* i0 = u32_sub i 1 in
+      let* tl0 = list_nth_mut_loop_with_id_loop_back t i0 tl ret in
+      Return (List_Cons x tl0)
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_with_id]: backward function 0 *)
+let list_nth_mut_loop_with_id_back
+  (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
+  let* ls0 = id_mut t ls in
+  let* l = list_nth_mut_loop_with_id_loop_back t i ls0 ret in
+  id_mut_back t ls l
+
+(** [loops::list_nth_shared_loop_with_id]: decreases clause *)
+unfold
+let list_nth_shared_loop_with_id_loop_decreases (t : Type0) (i : u32)
+  (ls : list_t t) : nat =
+  admit ()
+
+(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *)
+let rec list_nth_shared_loop_with_id_loop
+  (t : Type0) (i : u32) (ls : list_t t) :
+  Tot (result t)
+  (decreases (list_nth_shared_loop_with_id_loop_decreases t i ls))
+  =
+  begin match ls with
+  | List_Cons x tl ->
+    if i = 0
+    then Return x
+    else let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop t i0 tl
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_loop_with_id]: forward function *)
+let list_nth_shared_loop_with_id
+  (t : Type0) (ls : list_t t) (i : u32) : result t =
+  let* ls0 = id_shared t ls in list_nth_shared_loop_with_id_loop t i ls0
+
+(** [loops::list_nth_mut_loop_pair]: decreases clause *)
+unfold
+let list_nth_mut_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
+  admit ()
+
+(** [loops::list_nth_mut_loop_pair]: loop 0: forward function *)
+let rec list_nth_mut_loop_pair_loop
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop t tl0 tl1 i0
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair]: forward function *)
+let list_nth_mut_loop_pair
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_mut_loop_pair_loop t ls0 ls1 i
+
+(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *)
+let rec list_nth_mut_loop_pair_loop_back'a
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (List_Cons ret tl0)
+      else
+        let* i0 = u32_sub i 1 in
+        let* tl00 = list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret in
+        Return (List_Cons x0 tl00)
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair]: backward function 0 *)
+let list_nth_mut_loop_pair_back'a
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_mut_loop_pair_loop_back'a t ls0 ls1 i ret
+
+(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 *)
+let rec list_nth_mut_loop_pair_loop_back'b
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (List_Cons ret tl1)
+      else
+        let* i0 = u32_sub i 1 in
+        let* tl10 = list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret in
+        Return (List_Cons x1 tl10)
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair]: backward function 1 *)
+let list_nth_mut_loop_pair_back'b
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
+  admit ()
+
+(** [loops::list_nth_shared_loop_pair]: loop 0: forward function *)
+let rec list_nth_shared_loop_pair_loop
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_shared_loop_pair_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else let* i0 = u32_sub i 1 in list_nth_shared_loop_pair_loop t tl0 tl1 i0
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_loop_pair]: forward function *)
+let list_nth_shared_loop_pair
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_shared_loop_pair_loop t ls0 ls1 i
+
+(** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_mut_loop_pair_merge_loop_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
+  admit ()
+
+(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *)
+let rec list_nth_mut_loop_pair_merge_loop
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else
+        let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_merge_loop t tl0 tl1 i0
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair_merge]: forward function *)
+let list_nth_mut_loop_pair_merge
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_mut_loop_pair_merge_loop t ls0 ls1 i
+
+(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *)
+let rec list_nth_mut_loop_pair_merge_loop_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) :
+  Tot (result ((list_t t) & (list_t t)))
+  (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1)
+      else
+        let* i0 = u32_sub i 1 in
+        let* (tl00, tl10) =
+          list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
+        Return (List_Cons x0 tl00, List_Cons x1 tl10)
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *)
+let list_nth_mut_loop_pair_merge_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) :
+  result ((list_t t) & (list_t t))
+  =
+  list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_merge_loop_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
+  admit ()
+
+(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *)
+let rec list_nth_shared_loop_pair_merge_loop
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_shared_loop_pair_merge_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else
+        let* i0 = u32_sub i 1 in
+        list_nth_shared_loop_pair_merge_loop t tl0 tl1 i0
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_loop_pair_merge]: forward function *)
+let list_nth_shared_loop_pair_merge
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_shared_loop_pair_merge_loop t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
+  admit ()
+
+(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *)
+let rec list_nth_mut_shared_loop_pair_loop
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else
+        let* i0 = u32_sub i 1 in
+        list_nth_mut_shared_loop_pair_loop t tl0 tl1 i0
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_shared_loop_pair]: forward function *)
+let list_nth_mut_shared_loop_pair
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_mut_shared_loop_pair_loop t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *)
+let rec list_nth_mut_shared_loop_pair_loop_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (List_Cons ret tl0)
+      else
+        let* i0 = u32_sub i 1 in
+        let* tl00 = list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret in
+        Return (List_Cons x0 tl00)
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *)
+let list_nth_mut_shared_loop_pair_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_merge_loop_decreases (t : Type0)
+  (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat =
+  admit ()
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *)
+let rec list_nth_mut_shared_loop_pair_merge_loop
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else
+        let* i0 = u32_sub i 1 in
+        list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i0
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *)
+let list_nth_mut_shared_loop_pair_merge
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *)
+let rec list_nth_mut_shared_loop_pair_merge_loop_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (List_Cons ret tl0)
+      else
+        let* i0 = u32_sub i 1 in
+        let* tl00 =
+          list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
+        Return (List_Cons x0 tl00)
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *)
+let list_nth_mut_shared_loop_pair_merge_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
+  admit ()
+
+(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *)
+let rec list_nth_shared_mut_loop_pair_loop
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else
+        let* i0 = u32_sub i 1 in
+        list_nth_shared_mut_loop_pair_loop t tl0 tl1 i0
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_mut_loop_pair]: forward function *)
+let list_nth_shared_mut_loop_pair
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_shared_mut_loop_pair_loop t ls0 ls1 i
+
+(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *)
+let rec list_nth_shared_mut_loop_pair_loop_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (List_Cons ret tl1)
+      else
+        let* i0 = u32_sub i 1 in
+        let* tl10 = list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret in
+        Return (List_Cons x1 tl10)
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *)
+let list_nth_shared_mut_loop_pair_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0)
+  (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat =
+  admit ()
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *)
+let rec list_nth_shared_mut_loop_pair_merge_loop
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else
+        let* i0 = u32_sub i 1 in
+        list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i0
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *)
+let list_nth_shared_mut_loop_pair_merge
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *)
+let rec list_nth_shared_mut_loop_pair_merge_loop_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
+  =
+  begin match ls0 with
+  | List_Cons x0 tl0 ->
+    begin match ls1 with
+    | List_Cons x1 tl1 ->
+      if i = 0
+      then Return (List_Cons ret tl1)
+      else
+        let* i0 = u32_sub i 1 in
+        let* tl10 =
+          list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
+        Return (List_Cons x1 tl10)
+    | List_Nil -> Fail Failure
+    end
+  | List_Nil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *)
+let list_nth_shared_mut_loop_pair_merge_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_shared_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+
diff --git a/tests/lean/Array.lean b/tests/lean/Array.lean
index 277b63d9..20f02e97 100644
--- a/tests/lean/Array.lean
+++ b/tests/lean/Array.lean
@@ -1 +1,435 @@
-import Array.Funs
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [array]
+import Base
+open Primitives
+
+namespace array
+
+/- [array::AB] -/
+inductive AB :=
+| A : AB
+| B : AB
+
+/- [array::incr]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+def incr (x : U32) : Result U32 :=
+  x + 1#u32
+
+/- [array::array_to_shared_slice_]: forward function -/
+def array_to_shared_slice_
+  (T : Type) (s : Array T 32#usize) : Result (Slice T) :=
+  Array.to_slice T 32#usize s
+
+/- [array::array_to_mut_slice_]: forward function -/
+def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result (Slice T) :=
+  Array.to_slice T 32#usize s
+
+/- [array::array_to_mut_slice_]: backward function 0 -/
+def array_to_mut_slice__back
+  (T : Type) (s : Array T 32#usize) (ret0 : Slice T) :
+  Result (Array T 32#usize)
+  :=
+  Array.from_slice T 32#usize s ret0
+
+/- [array::array_len]: forward function -/
+def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
+  do
+    let s0 ← Array.to_slice T 32#usize s
+    let i := Slice.len T s0
+    Result.ret i
+
+/- [array::shared_array_len]: forward function -/
+def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
+  do
+    let s0 ← Array.to_slice T 32#usize s
+    let i := Slice.len T s0
+    Result.ret i
+
+/- [array::shared_slice_len]: forward function -/
+def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
+  let i := Slice.len T s
+  Result.ret i
+
+/- [array::index_array_shared]: forward function -/
+def index_array_shared
+  (T : Type) (s : Array T 32#usize) (i : Usize) : Result T :=
+  Array.index_usize T 32#usize s i
+
+/- [array::index_array_u32]: forward function -/
+def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 :=
+  Array.index_usize U32 32#usize s i
+
+/- [array::index_array_copy]: forward function -/
+def index_array_copy (x : Array U32 32#usize) : Result U32 :=
+  Array.index_usize U32 32#usize x 0#usize
+
+/- [array::index_mut_array]: forward function -/
+def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result T :=
+  Array.index_usize T 32#usize s i
+
+/- [array::index_mut_array]: backward function 0 -/
+def index_mut_array_back
+  (T : Type) (s : Array T 32#usize) (i : Usize) (ret0 : T) :
+  Result (Array T 32#usize)
+  :=
+  Array.update_usize T 32#usize s i ret0
+
+/- [array::index_slice]: forward function -/
+def index_slice (T : Type) (s : Slice T) (i : Usize) : Result T :=
+  Slice.index_usize T s i
+
+/- [array::index_mut_slice]: forward function -/
+def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result T :=
+  Slice.index_usize T s i
+
+/- [array::index_mut_slice]: backward function 0 -/
+def index_mut_slice_back
+  (T : Type) (s : Slice T) (i : Usize) (ret0 : T) : Result (Slice T) :=
+  Slice.update_usize T s i ret0
+
+/- [array::slice_subslice_shared_]: forward function -/
+def slice_subslice_shared_
+  (x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) :=
+  core.slice.index.Slice.index U32 (core.ops.range.Range Usize)
+    (core.slice.index.Range.coresliceindexSliceIndexInst U32) x
+    { start := y, end_ := z }
+
+/- [array::slice_subslice_mut_]: forward function -/
+def slice_subslice_mut_
+  (x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) :=
+  core.slice.index.Slice.index_mut U32 (core.ops.range.Range Usize)
+    (core.slice.index.Range.coresliceindexSliceIndexInst U32) x
+    { start := y, end_ := z }
+
+/- [array::slice_subslice_mut_]: backward function 0 -/
+def slice_subslice_mut__back
+  (x : Slice U32) (y : Usize) (z : Usize) (ret0 : Slice U32) :
+  Result (Slice U32)
+  :=
+  core.slice.index.Slice.index_mut_back U32 (core.ops.range.Range Usize)
+    (core.slice.index.Range.coresliceindexSliceIndexInst U32) x
+    { start := y, end_ := z } ret0
+
+/- [array::array_to_slice_shared_]: forward function -/
+def array_to_slice_shared_ (x : Array U32 32#usize) : Result (Slice U32) :=
+  Array.to_slice U32 32#usize x
+
+/- [array::array_to_slice_mut_]: forward function -/
+def array_to_slice_mut_ (x : Array U32 32#usize) : Result (Slice U32) :=
+  Array.to_slice U32 32#usize x
+
+/- [array::array_to_slice_mut_]: backward function 0 -/
+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
+
+/- [array::array_subslice_shared_]: forward function -/
+def array_subslice_shared_
+  (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
+  core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize
+    (core.slice.index.Slice.coreopsindexIndexInst U32 (core.ops.range.Range
+    Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x
+    { start := y, end_ := z }
+
+/- [array::array_subslice_mut_]: forward function -/
+def array_subslice_mut_
+  (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
+  core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize
+    (core.slice.index.Slice.coreopsindexIndexMutInst U32 (core.ops.range.Range
+    Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x
+    { start := y, end_ := z }
+
+/- [array::array_subslice_mut_]: backward function 0 -/
+def array_subslice_mut__back
+  (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret0 : Slice U32) :
+  Result (Array U32 32#usize)
+  :=
+  core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 32#usize
+    (core.slice.index.Slice.coreopsindexIndexMutInst U32 (core.ops.range.Range
+    Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x
+    { start := y, end_ := z } ret0
+
+/- [array::index_slice_0]: forward function -/
+def index_slice_0 (T : Type) (s : Slice T) : Result T :=
+  Slice.index_usize T s 0#usize
+
+/- [array::index_array_0]: forward function -/
+def index_array_0 (T : Type) (s : Array T 32#usize) : Result T :=
+  Array.index_usize T 32#usize s 0#usize
+
+/- [array::index_index_array]: forward function -/
+def index_index_array
+  (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
+  Result U32
+  :=
+  do
+    let a ← Array.index_usize (Array U32 32#usize) 32#usize s i
+    Array.index_usize U32 32#usize a j
+
+/- [array::update_update_array]: forward function -/
+def update_update_array
+  (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
+  Result Unit
+  :=
+  do
+    let a ← Array.index_usize (Array U32 32#usize) 32#usize s i
+    let a0 ← Array.update_usize U32 32#usize a j 0#u32
+    let _ ← Array.update_usize (Array U32 32#usize) 32#usize s i a0
+    Result.ret ()
+
+/- [array::array_local_deep_copy]: forward function -/
+def array_local_deep_copy (x : Array U32 32#usize) : Result Unit :=
+  Result.ret ()
+
+/- [array::take_array]: forward function -/
+def take_array (a : Array U32 2#usize) : Result Unit :=
+  Result.ret ()
+
+/- [array::take_array_borrow]: forward function -/
+def take_array_borrow (a : Array U32 2#usize) : Result Unit :=
+  Result.ret ()
+
+/- [array::take_slice]: forward function -/
+def take_slice (s : Slice U32) : Result Unit :=
+  Result.ret ()
+
+/- [array::take_mut_slice]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+def take_mut_slice (s : Slice U32) : Result (Slice U32) :=
+  Result.ret s
+
+/- [array::take_all]: forward function -/
+def take_all : Result Unit :=
+  do
+    let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let s ←
+      Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let _ ← take_slice s
+    let s0 ←
+      Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let s1 ← take_mut_slice s0
+    let _ ←
+      Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1
+    Result.ret ()
+
+/- [array::index_array]: forward function -/
+def index_array (x : Array U32 2#usize) : Result U32 :=
+  Array.index_usize U32 2#usize x 0#usize
+
+/- [array::index_array_borrow]: forward function -/
+def index_array_borrow (x : Array U32 2#usize) : Result U32 :=
+  Array.index_usize U32 2#usize x 0#usize
+
+/- [array::index_slice_u32_0]: forward function -/
+def index_slice_u32_0 (x : Slice U32) : Result U32 :=
+  Slice.index_usize U32 x 0#usize
+
+/- [array::index_mut_slice_u32_0]: forward function -/
+def index_mut_slice_u32_0 (x : Slice U32) : Result U32 :=
+  Slice.index_usize U32 x 0#usize
+
+/- [array::index_mut_slice_u32_0]: backward function 0 -/
+def index_mut_slice_u32_0_back (x : Slice U32) : Result (Slice U32) :=
+  do
+    let _ ← Slice.index_usize U32 x 0#usize
+    Result.ret x
+
+/- [array::index_all]: forward function -/
+def index_all : Result U32 :=
+  do
+    let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let i0 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let i1 ← i + i0
+    let i2 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let i3 ← i1 + i2
+    let s ←
+      Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let i4 ← index_slice_u32_0 s
+    let i5 ← i3 + i4
+    let s0 ←
+      Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let i6 ← index_mut_slice_u32_0 s0
+    let i7 ← i5 + i6
+    let s1 ← index_mut_slice_u32_0_back s0
+    let _ ←
+      Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1
+    Result.ret i7
+
+/- [array::update_array]: forward function -/
+def update_array (x : Array U32 2#usize) : Result Unit :=
+  do
+    let _ ← Array.update_usize U32 2#usize x 0#usize 1#u32
+    Result.ret ()
+
+/- [array::update_array_mut_borrow]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+def update_array_mut_borrow
+  (x : Array U32 2#usize) : Result (Array U32 2#usize) :=
+  Array.update_usize U32 2#usize x 0#usize 1#u32
+
+/- [array::update_mut_slice]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+def update_mut_slice (x : Slice U32) : Result (Slice U32) :=
+  Slice.update_usize U32 x 0#usize 1#u32
+
+/- [array::update_all]: forward function -/
+def update_all : Result Unit :=
+  do
+    let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let s ← Array.to_slice U32 2#usize x
+    let s0 ← update_mut_slice s
+    let _ ← Array.from_slice U32 2#usize x s0
+    Result.ret ()
+
+/- [array::range_all]: forward function -/
+def range_all : Result Unit :=
+  do
+    let s ←
+      core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize
+        (core.slice.index.Slice.coreopsindexIndexMutInst U32
+        (core.ops.range.Range Usize)
+        (core.slice.index.Range.coresliceindexSliceIndexInst U32))
+        (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ])
+        { start := 1#usize, end_ := 3#usize }
+    let s0 ← update_mut_slice s
+    let _ ←
+      core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 4#usize
+        (core.slice.index.Slice.coreopsindexIndexMutInst U32
+        (core.ops.range.Range Usize)
+        (core.slice.index.Range.coresliceindexSliceIndexInst U32))
+        (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ])
+        { start := 1#usize, end_ := 3#usize } s0
+    Result.ret ()
+
+/- [array::deref_array_borrow]: forward function -/
+def deref_array_borrow (x : Array U32 2#usize) : Result U32 :=
+  Array.index_usize U32 2#usize x 0#usize
+
+/- [array::deref_array_mut_borrow]: forward function -/
+def deref_array_mut_borrow (x : Array U32 2#usize) : Result U32 :=
+  Array.index_usize U32 2#usize x 0#usize
+
+/- [array::deref_array_mut_borrow]: backward function 0 -/
+def deref_array_mut_borrow_back
+  (x : Array U32 2#usize) : Result (Array U32 2#usize) :=
+  do
+    let _ ← Array.index_usize U32 2#usize x 0#usize
+    Result.ret x
+
+/- [array::take_array_t]: forward function -/
+def take_array_t (a : Array AB 2#usize) : Result Unit :=
+  Result.ret ()
+
+/- [array::non_copyable_array]: forward function -/
+def non_copyable_array : Result Unit :=
+  do
+    let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
+    Result.ret ()
+
+/- [array::sum]: loop 0: forward function -/
+divergent def sum_loop (s : Slice U32) (sum0 : U32) (i : Usize) : Result U32 :=
+  let i0 := Slice.len U32 s
+  if i < i0
+  then
+    do
+      let i1 ← Slice.index_usize U32 s i
+      let sum1 ← sum0 + i1
+      let i2 ← i + 1#usize
+      sum_loop s sum1 i2
+  else Result.ret sum0
+
+/- [array::sum]: forward function -/
+def sum (s : Slice U32) : Result U32 :=
+  sum_loop s 0#u32 0#usize
+
+/- [array::sum2]: loop 0: forward function -/
+divergent def sum2_loop
+  (s : Slice U32) (s2 : Slice U32) (sum0 : U32) (i : Usize) : Result U32 :=
+  let i0 := Slice.len U32 s
+  if i < i0
+  then
+    do
+      let i1 ← Slice.index_usize U32 s i
+      let i2 ← Slice.index_usize U32 s2 i
+      let i3 ← i1 + i2
+      let sum1 ← sum0 + i3
+      let i4 ← i + 1#usize
+      sum2_loop s s2 sum1 i4
+  else Result.ret sum0
+
+/- [array::sum2]: forward function -/
+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
+  else sum2_loop s s2 0#u32 0#usize
+
+/- [array::f0]: forward function -/
+def f0 : Result Unit :=
+  do
+    let s ←
+      Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+    let s0 ← Slice.update_usize U32 s 0#usize 1#u32
+    let _ ←
+      Array.from_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) s0
+    Result.ret ()
+
+/- [array::f1]: forward function -/
+def f1 : Result Unit :=
+  do
+    let _ ←
+      Array.update_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+        0#usize 1#u32
+    Result.ret ()
+
+/- [array::f2]: forward function -/
+def f2 (i : U32) : Result Unit :=
+  Result.ret ()
+
+/- [array::f4]: forward function -/
+def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
+  core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize
+    (core.slice.index.Slice.coreopsindexIndexInst U32 (core.ops.range.Range
+    Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x
+    { start := y, end_ := z }
+
+/- [array::f3]: forward function -/
+def f3 : Result U32 :=
+  do
+    let i ←
+      Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+        0#usize
+    let _ ← f2 i
+    let b := Array.repeat U32 32#usize 0#u32
+    let s ←
+      Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+    let s0 ← f4 b 16#usize 18#usize
+    sum2 s s0
+
+/- [array::SZ] -/
+def sz_body : Result Usize := Result.ret 32#usize
+def sz_c : Usize := eval_global sz_body (by simp)
+
+/- [array::f5]: forward function -/
+def f5 (x : Array U32 32#usize) : Result U32 :=
+  Array.index_usize U32 32#usize x 0#usize
+
+/- [array::ite]: forward function -/
+def ite : Result Unit :=
+  do
+    let s ←
+      Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let s0 ←
+      Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    let s1 ← index_mut_slice_u32_0_back s0
+    let _ ←
+      Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1
+    let s2 ← index_mut_slice_u32_0_back s
+    let _ ←
+      Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s2
+    Result.ret ()
+
+end array
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 60c73776..c6360338 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -1 +1,629 @@
-import Loops.Funs
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [loops]
+import Base
+open Primitives
+
+namespace loops
+
+/- [loops::sum]: loop 0: forward function -/
+divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
+  if i < max
+  then do
+         let s0 ← s + i
+         let i0 ← i + 1#u32
+         sum_loop max i0 s0
+  else s * 2#u32
+
+/- [loops::sum]: forward function -/
+def sum (max : U32) : Result U32 :=
+  sum_loop max 0#u32 0#u32
+
+/- [loops::sum_with_mut_borrows]: loop 0: forward function -/
+divergent def sum_with_mut_borrows_loop
+  (max : U32) (mi : U32) (ms : U32) : Result U32 :=
+  if mi < max
+  then
+    do
+      let ms0 ← ms + mi
+      let mi0 ← mi + 1#u32
+      sum_with_mut_borrows_loop max mi0 ms0
+  else ms * 2#u32
+
+/- [loops::sum_with_mut_borrows]: forward function -/
+def sum_with_mut_borrows (max : U32) : Result U32 :=
+  sum_with_mut_borrows_loop max 0#u32 0#u32
+
+/- [loops::sum_with_shared_borrows]: loop 0: forward function -/
+divergent def sum_with_shared_borrows_loop
+  (max : U32) (i : U32) (s : U32) : Result U32 :=
+  if i < max
+  then
+    do
+      let i0 ← i + 1#u32
+      let s0 ← s + i0
+      sum_with_shared_borrows_loop max i0 s0
+  else s * 2#u32
+
+/- [loops::sum_with_shared_borrows]: forward function -/
+def sum_with_shared_borrows (max : U32) : Result U32 :=
+  sum_with_shared_borrows_loop max 0#u32 0#u32
+
+/- [loops::clear]: loop 0: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+divergent def clear_loop
+  (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
+  let i0 := alloc.vec.Vec.len U32 v
+  if i < i0
+  then
+    do
+      let i1 ← i + 1#usize
+      let v0 ←
+        alloc.vec.Vec.index_mut_back U32 Usize
+          (core.slice.index.usize.coresliceindexSliceIndexInst U32) v i 0#u32
+      clear_loop v0 i1
+  else Result.ret v
+
+/- [loops::clear]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
+  clear_loop v 0#usize
+
+/- [loops::List] -/
+inductive List (T : Type) :=
+| Cons : T → List T → List T
+| Nil : List T
+
+/- [loops::list_mem]: loop 0: forward function -/
+divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
+  match ls with
+  | List.Cons y tl => if y = x
+                      then Result.ret true
+                      else list_mem_loop x tl
+  | List.Nil => Result.ret false
+
+/- [loops::list_mem]: forward function -/
+def list_mem (x : U32) (ls : List U32) : Result Bool :=
+  list_mem_loop x ls
+
+/- [loops::list_nth_mut_loop]: loop 0: forward function -/
+divergent def list_nth_mut_loop_loop
+  (T : Type) (ls : List T) (i : U32) : Result T :=
+  match ls with
+  | List.Cons x tl =>
+    if i = 0#u32
+    then Result.ret x
+    else do
+           let i0 ← i - 1#u32
+           list_nth_mut_loop_loop T tl i0
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop]: forward function -/
+def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T :=
+  list_nth_mut_loop_loop T ls i
+
+/- [loops::list_nth_mut_loop]: loop 0: backward function 0 -/
+divergent def list_nth_mut_loop_loop_back
+  (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
+  match ls with
+  | List.Cons x tl =>
+    if i = 0#u32
+    then Result.ret (List.Cons ret0 tl)
+    else
+      do
+        let i0 ← i - 1#u32
+        let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
+        Result.ret (List.Cons x tl0)
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop]: backward function 0 -/
+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
+
+/- [loops::list_nth_shared_loop]: loop 0: forward function -/
+divergent def list_nth_shared_loop_loop
+  (T : Type) (ls : List T) (i : U32) : Result T :=
+  match ls with
+  | List.Cons x tl =>
+    if i = 0#u32
+    then Result.ret x
+    else do
+           let i0 ← i - 1#u32
+           list_nth_shared_loop_loop T tl i0
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_loop]: forward function -/
+def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T :=
+  list_nth_shared_loop_loop T ls i
+
+/- [loops::get_elem_mut]: loop 0: forward function -/
+divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize :=
+  match ls with
+  | List.Cons y tl => if y = x
+                      then Result.ret y
+                      else get_elem_mut_loop x tl
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::get_elem_mut]: forward function -/
+def get_elem_mut
+  (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
+  do
+    let l ←
+      alloc.vec.Vec.index_mut (List Usize) Usize
+        (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize))
+        slots 0#usize
+    get_elem_mut_loop x l
+
+/- [loops::get_elem_mut]: loop 0: backward function 0 -/
+divergent def get_elem_mut_loop_back
+  (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) :=
+  match ls with
+  | List.Cons y tl =>
+    if y = x
+    then Result.ret (List.Cons ret0 tl)
+    else
+      do
+        let tl0 ← get_elem_mut_loop_back x tl ret0
+        Result.ret (List.Cons y tl0)
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::get_elem_mut]: backward function 0 -/
+def get_elem_mut_back
+  (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret0 : Usize) :
+  Result (alloc.vec.Vec (List Usize))
+  :=
+  do
+    let l ←
+      alloc.vec.Vec.index_mut (List Usize) Usize
+        (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize))
+        slots 0#usize
+    let l0 ← get_elem_mut_loop_back x l ret0
+    alloc.vec.Vec.index_mut_back (List Usize) Usize
+      (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) slots
+      0#usize l0
+
+/- [loops::get_elem_shared]: loop 0: forward function -/
+divergent def get_elem_shared_loop
+  (x : Usize) (ls : List Usize) : Result Usize :=
+  match ls with
+  | List.Cons y tl => if y = x
+                      then Result.ret y
+                      else get_elem_shared_loop x tl
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::get_elem_shared]: forward function -/
+def get_elem_shared
+  (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
+  do
+    let l ←
+      alloc.vec.Vec.index (List Usize) Usize
+        (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize))
+        slots 0#usize
+    get_elem_shared_loop x l
+
+/- [loops::id_mut]: forward function -/
+def id_mut (T : Type) (ls : List T) : Result (List T) :=
+  Result.ret ls
+
+/- [loops::id_mut]: backward function 0 -/
+def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) :=
+  Result.ret ret0
+
+/- [loops::id_shared]: forward function -/
+def id_shared (T : Type) (ls : List T) : Result (List T) :=
+  Result.ret ls
+
+/- [loops::list_nth_mut_loop_with_id]: loop 0: forward function -/
+divergent def list_nth_mut_loop_with_id_loop
+  (T : Type) (i : U32) (ls : List T) : Result T :=
+  match ls with
+  | List.Cons x tl =>
+    if i = 0#u32
+    then Result.ret x
+    else do
+           let i0 ← i - 1#u32
+           list_nth_mut_loop_with_id_loop T i0 tl
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_with_id]: forward function -/
+def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T :=
+  do
+    let ls0 ← id_mut T ls
+    list_nth_mut_loop_with_id_loop T i ls0
+
+/- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 -/
+divergent def list_nth_mut_loop_with_id_loop_back
+  (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) :=
+  match ls with
+  | List.Cons x tl =>
+    if i = 0#u32
+    then Result.ret (List.Cons ret0 tl)
+    else
+      do
+        let i0 ← i - 1#u32
+        let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
+        Result.ret (List.Cons x tl0)
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_with_id]: backward function 0 -/
+def list_nth_mut_loop_with_id_back
+  (T : Type) (ls : List T) (i : U32) (ret0 : 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
+    id_mut_back T ls l
+
+/- [loops::list_nth_shared_loop_with_id]: loop 0: forward function -/
+divergent def list_nth_shared_loop_with_id_loop
+  (T : Type) (i : U32) (ls : List T) : Result T :=
+  match ls with
+  | List.Cons x tl =>
+    if i = 0#u32
+    then Result.ret x
+    else do
+           let i0 ← i - 1#u32
+           list_nth_shared_loop_with_id_loop T i0 tl
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_loop_with_id]: forward function -/
+def list_nth_shared_loop_with_id
+  (T : Type) (ls : List T) (i : U32) : Result T :=
+  do
+    let ls0 ← id_shared T ls
+    list_nth_shared_loop_with_id_loop T i ls0
+
+/- [loops::list_nth_mut_loop_pair]: loop 0: forward function -/
+divergent def list_nth_mut_loop_pair_loop
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (x0, x1)
+      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
+
+/- [loops::list_nth_mut_loop_pair]: forward function -/
+def list_nth_mut_loop_pair
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  list_nth_mut_loop_pair_loop T ls0 ls1 i
+
+/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 -/
+divergent def list_nth_mut_loop_pair_loop_back'a
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (List.Cons ret0 tl0)
+      else
+        do
+          let i0 ← i - 1#u32
+          let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
+          Result.ret (List.Cons x0 tl00)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_pair]: backward function 0 -/
+def list_nth_mut_loop_pair_back'a
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0
+
+/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 -/
+divergent def list_nth_mut_loop_pair_loop_back'b
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (List.Cons ret0 tl1)
+      else
+        do
+          let i0 ← i - 1#u32
+          let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
+          Result.ret (List.Cons x1 tl10)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_pair]: backward function 1 -/
+def list_nth_mut_loop_pair_back'b
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0
+
+/- [loops::list_nth_shared_loop_pair]: loop 0: forward function -/
+divergent def list_nth_shared_loop_pair_loop
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (x0, x1)
+      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
+
+/- [loops::list_nth_shared_loop_pair]: forward function -/
+def list_nth_shared_loop_pair
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  list_nth_shared_loop_pair_loop T ls0 ls1 i
+
+/- [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function -/
+divergent def list_nth_mut_loop_pair_merge_loop
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (x0, x1)
+      else
+        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
+
+/- [loops::list_nth_mut_loop_pair_merge]: forward function -/
+def list_nth_mut_loop_pair_merge
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
+
+/- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 -/
+divergent def list_nth_mut_loop_pair_merge_loop_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
+  Result ((List T) × (List T))
+  :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then let (t, t0) := ret0
+           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
+          Result.ret (List.Cons x0 tl00, List.Cons x1 tl10)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_pair_merge]: backward function 0 -/
+def list_nth_mut_loop_pair_merge_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
+  Result ((List T) × (List T))
+  :=
+  list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
+
+/- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function -/
+divergent def list_nth_shared_loop_pair_merge_loop
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (x0, x1)
+      else
+        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
+
+/- [loops::list_nth_shared_loop_pair_merge]: forward function -/
+def list_nth_shared_loop_pair_merge
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  list_nth_shared_loop_pair_merge_loop T ls0 ls1 i
+
+/- [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function -/
+divergent def list_nth_mut_shared_loop_pair_loop
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (x0, x1)
+      else
+        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
+
+/- [loops::list_nth_mut_shared_loop_pair]: forward function -/
+def list_nth_mut_shared_loop_pair
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
+
+/- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 -/
+divergent def list_nth_mut_shared_loop_pair_loop_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (List.Cons ret0 tl0)
+      else
+        do
+          let i0 ← i - 1#u32
+          let tl00 ←
+            list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
+          Result.ret (List.Cons x0 tl00)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_shared_loop_pair]: backward function 0 -/
+def list_nth_mut_shared_loop_pair_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0
+
+/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function -/
+divergent def list_nth_mut_shared_loop_pair_merge_loop
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (x0, x1)
+      else
+        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
+
+/- [loops::list_nth_mut_shared_loop_pair_merge]: forward function -/
+def list_nth_mut_shared_loop_pair_merge
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
+
+/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 -/
+divergent def list_nth_mut_shared_loop_pair_merge_loop_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (List.Cons ret0 tl0)
+      else
+        do
+          let i0 ← i - 1#u32
+          let tl00 ←
+            list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+          Result.ret (List.Cons x0 tl00)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 -/
+def list_nth_mut_shared_loop_pair_merge_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0
+
+/- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function -/
+divergent def list_nth_shared_mut_loop_pair_loop
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (x0, x1)
+      else
+        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
+
+/- [loops::list_nth_shared_mut_loop_pair]: forward function -/
+def list_nth_shared_mut_loop_pair
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
+
+/- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 -/
+divergent def list_nth_shared_mut_loop_pair_loop_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (List.Cons ret0 tl1)
+      else
+        do
+          let i0 ← i - 1#u32
+          let tl10 ←
+            list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
+          Result.ret (List.Cons x1 tl10)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_mut_loop_pair]: backward function 1 -/
+def list_nth_shared_mut_loop_pair_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0
+
+/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function -/
+divergent def list_nth_shared_mut_loop_pair_merge_loop
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (x0, x1)
+      else
+        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
+
+/- [loops::list_nth_shared_mut_loop_pair_merge]: forward function -/
+def list_nth_shared_mut_loop_pair_merge
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
+  list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
+
+/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 -/
+divergent def list_nth_shared_mut_loop_pair_merge_loop_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  match ls0 with
+  | List.Cons x0 tl0 =>
+    match ls1 with
+    | List.Cons x1 tl1 =>
+      if i = 0#u32
+      then Result.ret (List.Cons ret0 tl1)
+      else
+        do
+          let i0 ← i - 1#u32
+          let tl10 ←
+            list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+          Result.ret (List.Cons x1 tl10)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 -/
+def list_nth_shared_mut_loop_pair_merge_back
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
+  :=
+  list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
+
+end loops
diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
deleted file mode 100644
index f9c7569e..00000000
--- a/tests/lean/Loops/Funs.lean
+++ /dev/null
@@ -1,625 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [loops]: function definitions
-import Base
-import Loops.Types
-open Primitives
-
-namespace loops
-
-/- [loops::sum]: loop 0: forward function -/
-divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
-  if i < max
-  then do
-         let s0 ← s + i
-         let i0 ← i + 1#u32
-         sum_loop max i0 s0
-  else s * 2#u32
-
-/- [loops::sum]: forward function -/
-def sum (max : U32) : Result U32 :=
-  sum_loop max 0#u32 0#u32
-
-/- [loops::sum_with_mut_borrows]: loop 0: forward function -/
-divergent def sum_with_mut_borrows_loop
-  (max : U32) (mi : U32) (ms : U32) : Result U32 :=
-  if mi < max
-  then
-    do
-      let ms0 ← ms + mi
-      let mi0 ← mi + 1#u32
-      sum_with_mut_borrows_loop max mi0 ms0
-  else ms * 2#u32
-
-/- [loops::sum_with_mut_borrows]: forward function -/
-def sum_with_mut_borrows (max : U32) : Result U32 :=
-  sum_with_mut_borrows_loop max 0#u32 0#u32
-
-/- [loops::sum_with_shared_borrows]: loop 0: forward function -/
-divergent def sum_with_shared_borrows_loop
-  (max : U32) (i : U32) (s : U32) : Result U32 :=
-  if i < max
-  then
-    do
-      let i0 ← i + 1#u32
-      let s0 ← s + i0
-      sum_with_shared_borrows_loop max i0 s0
-  else s * 2#u32
-
-/- [loops::sum_with_shared_borrows]: forward function -/
-def sum_with_shared_borrows (max : U32) : Result U32 :=
-  sum_with_shared_borrows_loop max 0#u32 0#u32
-
-/- [loops::clear]: loop 0: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
-divergent def clear_loop
-  (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
-  let i0 := alloc.vec.Vec.len U32 v
-  if i < i0
-  then
-    do
-      let i1 ← i + 1#usize
-      let v0 ←
-        alloc.vec.Vec.index_mut_back U32 Usize
-          (core.slice.index.usize.coresliceindexSliceIndexInst U32) v i 0#u32
-      clear_loop v0 i1
-  else Result.ret v
-
-/- [loops::clear]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
-def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
-  clear_loop v 0#usize
-
-/- [loops::list_mem]: loop 0: forward function -/
-divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
-  match ls with
-  | List.Cons y tl => if y = x
-                      then Result.ret true
-                      else list_mem_loop x tl
-  | List.Nil => Result.ret false
-
-/- [loops::list_mem]: forward function -/
-def list_mem (x : U32) (ls : List U32) : Result Bool :=
-  list_mem_loop x ls
-
-/- [loops::list_nth_mut_loop]: loop 0: forward function -/
-divergent def list_nth_mut_loop_loop
-  (T : Type) (ls : List T) (i : U32) : Result T :=
-  match ls with
-  | List.Cons x tl =>
-    if i = 0#u32
-    then Result.ret x
-    else do
-           let i0 ← i - 1#u32
-           list_nth_mut_loop_loop T tl i0
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_mut_loop]: forward function -/
-def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T :=
-  list_nth_mut_loop_loop T ls i
-
-/- [loops::list_nth_mut_loop]: loop 0: backward function 0 -/
-divergent def list_nth_mut_loop_loop_back
-  (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
-  match ls with
-  | List.Cons x tl =>
-    if i = 0#u32
-    then Result.ret (List.Cons ret0 tl)
-    else
-      do
-        let i0 ← i - 1#u32
-        let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
-        Result.ret (List.Cons x tl0)
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_mut_loop]: backward function 0 -/
-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
-
-/- [loops::list_nth_shared_loop]: loop 0: forward function -/
-divergent def list_nth_shared_loop_loop
-  (T : Type) (ls : List T) (i : U32) : Result T :=
-  match ls with
-  | List.Cons x tl =>
-    if i = 0#u32
-    then Result.ret x
-    else do
-           let i0 ← i - 1#u32
-           list_nth_shared_loop_loop T tl i0
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_shared_loop]: forward function -/
-def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T :=
-  list_nth_shared_loop_loop T ls i
-
-/- [loops::get_elem_mut]: loop 0: forward function -/
-divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize :=
-  match ls with
-  | List.Cons y tl => if y = x
-                      then Result.ret y
-                      else get_elem_mut_loop x tl
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::get_elem_mut]: forward function -/
-def get_elem_mut
-  (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
-  do
-    let l ←
-      alloc.vec.Vec.index_mut (List Usize) Usize
-        (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize))
-        slots 0#usize
-    get_elem_mut_loop x l
-
-/- [loops::get_elem_mut]: loop 0: backward function 0 -/
-divergent def get_elem_mut_loop_back
-  (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) :=
-  match ls with
-  | List.Cons y tl =>
-    if y = x
-    then Result.ret (List.Cons ret0 tl)
-    else
-      do
-        let tl0 ← get_elem_mut_loop_back x tl ret0
-        Result.ret (List.Cons y tl0)
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::get_elem_mut]: backward function 0 -/
-def get_elem_mut_back
-  (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret0 : Usize) :
-  Result (alloc.vec.Vec (List Usize))
-  :=
-  do
-    let l ←
-      alloc.vec.Vec.index_mut (List Usize) Usize
-        (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize))
-        slots 0#usize
-    let l0 ← get_elem_mut_loop_back x l ret0
-    alloc.vec.Vec.index_mut_back (List Usize) Usize
-      (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) slots
-      0#usize l0
-
-/- [loops::get_elem_shared]: loop 0: forward function -/
-divergent def get_elem_shared_loop
-  (x : Usize) (ls : List Usize) : Result Usize :=
-  match ls with
-  | List.Cons y tl => if y = x
-                      then Result.ret y
-                      else get_elem_shared_loop x tl
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::get_elem_shared]: forward function -/
-def get_elem_shared
-  (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
-  do
-    let l ←
-      alloc.vec.Vec.index (List Usize) Usize
-        (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize))
-        slots 0#usize
-    get_elem_shared_loop x l
-
-/- [loops::id_mut]: forward function -/
-def id_mut (T : Type) (ls : List T) : Result (List T) :=
-  Result.ret ls
-
-/- [loops::id_mut]: backward function 0 -/
-def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) :=
-  Result.ret ret0
-
-/- [loops::id_shared]: forward function -/
-def id_shared (T : Type) (ls : List T) : Result (List T) :=
-  Result.ret ls
-
-/- [loops::list_nth_mut_loop_with_id]: loop 0: forward function -/
-divergent def list_nth_mut_loop_with_id_loop
-  (T : Type) (i : U32) (ls : List T) : Result T :=
-  match ls with
-  | List.Cons x tl =>
-    if i = 0#u32
-    then Result.ret x
-    else do
-           let i0 ← i - 1#u32
-           list_nth_mut_loop_with_id_loop T i0 tl
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_mut_loop_with_id]: forward function -/
-def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T :=
-  do
-    let ls0 ← id_mut T ls
-    list_nth_mut_loop_with_id_loop T i ls0
-
-/- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 -/
-divergent def list_nth_mut_loop_with_id_loop_back
-  (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) :=
-  match ls with
-  | List.Cons x tl =>
-    if i = 0#u32
-    then Result.ret (List.Cons ret0 tl)
-    else
-      do
-        let i0 ← i - 1#u32
-        let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
-        Result.ret (List.Cons x tl0)
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_mut_loop_with_id]: backward function 0 -/
-def list_nth_mut_loop_with_id_back
-  (T : Type) (ls : List T) (i : U32) (ret0 : 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
-    id_mut_back T ls l
-
-/- [loops::list_nth_shared_loop_with_id]: loop 0: forward function -/
-divergent def list_nth_shared_loop_with_id_loop
-  (T : Type) (i : U32) (ls : List T) : Result T :=
-  match ls with
-  | List.Cons x tl =>
-    if i = 0#u32
-    then Result.ret x
-    else do
-           let i0 ← i - 1#u32
-           list_nth_shared_loop_with_id_loop T i0 tl
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_shared_loop_with_id]: forward function -/
-def list_nth_shared_loop_with_id
-  (T : Type) (ls : List T) (i : U32) : Result T :=
-  do
-    let ls0 ← id_shared T ls
-    list_nth_shared_loop_with_id_loop T i ls0
-
-/- [loops::list_nth_mut_loop_pair]: loop 0: forward function -/
-divergent def list_nth_mut_loop_pair_loop
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (x0, x1)
-      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
-
-/- [loops::list_nth_mut_loop_pair]: forward function -/
-def list_nth_mut_loop_pair
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_mut_loop_pair_loop T ls0 ls1 i
-
-/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 -/
-divergent def list_nth_mut_loop_pair_loop_back'a
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (List.Cons ret0 tl0)
-      else
-        do
-          let i0 ← i - 1#u32
-          let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
-          Result.ret (List.Cons x0 tl00)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_mut_loop_pair]: backward function 0 -/
-def list_nth_mut_loop_pair_back'a
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0
-
-/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 -/
-divergent def list_nth_mut_loop_pair_loop_back'b
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (List.Cons ret0 tl1)
-      else
-        do
-          let i0 ← i - 1#u32
-          let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
-          Result.ret (List.Cons x1 tl10)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_mut_loop_pair]: backward function 1 -/
-def list_nth_mut_loop_pair_back'b
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0
-
-/- [loops::list_nth_shared_loop_pair]: loop 0: forward function -/
-divergent def list_nth_shared_loop_pair_loop
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (x0, x1)
-      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
-
-/- [loops::list_nth_shared_loop_pair]: forward function -/
-def list_nth_shared_loop_pair
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_shared_loop_pair_loop T ls0 ls1 i
-
-/- [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function -/
-divergent def list_nth_mut_loop_pair_merge_loop
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (x0, x1)
-      else
-        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
-
-/- [loops::list_nth_mut_loop_pair_merge]: forward function -/
-def list_nth_mut_loop_pair_merge
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
-
-/- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 -/
-divergent def list_nth_mut_loop_pair_merge_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
-  Result ((List T) × (List T))
-  :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then let (t, t0) := ret0
-           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
-          Result.ret (List.Cons x0 tl00, List.Cons x1 tl10)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_mut_loop_pair_merge]: backward function 0 -/
-def list_nth_mut_loop_pair_merge_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
-  Result ((List T) × (List T))
-  :=
-  list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
-
-/- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function -/
-divergent def list_nth_shared_loop_pair_merge_loop
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (x0, x1)
-      else
-        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
-
-/- [loops::list_nth_shared_loop_pair_merge]: forward function -/
-def list_nth_shared_loop_pair_merge
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_shared_loop_pair_merge_loop T ls0 ls1 i
-
-/- [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function -/
-divergent def list_nth_mut_shared_loop_pair_loop
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (x0, x1)
-      else
-        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
-
-/- [loops::list_nth_mut_shared_loop_pair]: forward function -/
-def list_nth_mut_shared_loop_pair
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
-
-/- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 -/
-divergent def list_nth_mut_shared_loop_pair_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (List.Cons ret0 tl0)
-      else
-        do
-          let i0 ← i - 1#u32
-          let tl00 ←
-            list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
-          Result.ret (List.Cons x0 tl00)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_mut_shared_loop_pair]: backward function 0 -/
-def list_nth_mut_shared_loop_pair_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0
-
-/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function -/
-divergent def list_nth_mut_shared_loop_pair_merge_loop
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (x0, x1)
-      else
-        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
-
-/- [loops::list_nth_mut_shared_loop_pair_merge]: forward function -/
-def list_nth_mut_shared_loop_pair_merge
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
-
-/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 -/
-divergent def list_nth_mut_shared_loop_pair_merge_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (List.Cons ret0 tl0)
-      else
-        do
-          let i0 ← i - 1#u32
-          let tl00 ←
-            list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (List.Cons x0 tl00)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 -/
-def list_nth_mut_shared_loop_pair_merge_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0
-
-/- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function -/
-divergent def list_nth_shared_mut_loop_pair_loop
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (x0, x1)
-      else
-        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
-
-/- [loops::list_nth_shared_mut_loop_pair]: forward function -/
-def list_nth_shared_mut_loop_pair
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
-
-/- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 -/
-divergent def list_nth_shared_mut_loop_pair_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (List.Cons ret0 tl1)
-      else
-        do
-          let i0 ← i - 1#u32
-          let tl10 ←
-            list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
-          Result.ret (List.Cons x1 tl10)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_shared_mut_loop_pair]: backward function 1 -/
-def list_nth_shared_mut_loop_pair_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0
-
-/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function -/
-divergent def list_nth_shared_mut_loop_pair_merge_loop
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (x0, x1)
-      else
-        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
-
-/- [loops::list_nth_shared_mut_loop_pair_merge]: forward function -/
-def list_nth_shared_mut_loop_pair_merge
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
-
-/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 -/
-divergent def list_nth_shared_mut_loop_pair_merge_loop_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  match ls0 with
-  | List.Cons x0 tl0 =>
-    match ls1 with
-    | List.Cons x1 tl1 =>
-      if i = 0#u32
-      then Result.ret (List.Cons ret0 tl1)
-      else
-        do
-          let i0 ← i - 1#u32
-          let tl10 ←
-            list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (List.Cons x1 tl10)
-    | List.Nil => Result.fail Error.panic
-  | List.Nil => Result.fail Error.panic
-
-/- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 -/
-def list_nth_shared_mut_loop_pair_merge_back
-  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
-  Result (List T)
-  :=
-  list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
-
-end loops
diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean
deleted file mode 100644
index 018af901..00000000
--- a/tests/lean/Loops/Types.lean
+++ /dev/null
@@ -1,13 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [loops]: type definitions
-import Base
-open Primitives
-
-namespace loops
-
-/- [loops::List] -/
-inductive List (T : Type) :=
-| Cons : T → List T → List T
-| Nil : List T
-
-end loops
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 5e812e95..94ae0bb0 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -1 +1,410 @@
-import Traits.Funs
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [traits]
+import Base
+open Primitives
+
+namespace traits
+
+/- Trait declaration: [traits::BoolTrait] -/
+structure BoolTrait (Self : Type) where
+  get_bool : Self → Result Bool
+
+/- [traits::Bool::{0}::get_bool]: forward function -/
+def Bool.get_bool (self : Bool) : Result Bool :=
+  Result.ret self
+
+/- Trait implementation: [traits::Bool::{0}] -/
+def Bool.BoolTraitInst : BoolTrait Bool := {
+  get_bool := Bool.get_bool
+}
+
+/- [traits::BoolTrait::ret_true]: forward function -/
+def BoolTrait.ret_true
+  {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=
+  Result.ret true
+
+/- [traits::test_bool_trait_bool]: forward function -/
+def test_bool_trait_bool (x : Bool) : Result Bool :=
+  do
+    let b ← Bool.get_bool x
+    if b
+    then BoolTrait.ret_true Bool.BoolTraitInst x
+    else Result.ret false
+
+/- [traits::Option::{1}::get_bool]: forward function -/
+def Option.get_bool (T : Type) (self : Option T) : Result Bool :=
+  match self with
+  | none => Result.ret false
+  | some t => Result.ret true
+
+/- Trait implementation: [traits::Option::{1}] -/
+def Option.BoolTraitInst (T : Type) : BoolTrait (Option T) := {
+  get_bool := Option.get_bool T
+}
+
+/- [traits::test_bool_trait_option]: forward function -/
+def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
+  do
+    let b ← Option.get_bool T x
+    if b
+    then BoolTrait.ret_true (Option.BoolTraitInst T) x
+    else Result.ret false
+
+/- [traits::test_bool_trait]: forward function -/
+def test_bool_trait (T : Type) (inst : BoolTrait T) (x : T) : Result Bool :=
+  inst.get_bool x
+
+/- Trait declaration: [traits::ToU64] -/
+structure ToU64 (Self : Type) where
+  to_u64 : Self → Result U64
+
+/- [traits::u64::{2}::to_u64]: forward function -/
+def u64.to_u64 (self : U64) : Result U64 :=
+  Result.ret self
+
+/- Trait implementation: [traits::u64::{2}] -/
+def u64.ToU64Inst : ToU64 U64 := {
+  to_u64 := u64.to_u64
+}
+
+/- [traits::Tuple2::{3}::to_u64]: forward function -/
+def Tuple2.to_u64 (A : Type) (inst : ToU64 A) (self : (A × A)) : Result U64 :=
+  do
+    let (t, t0) := self
+    let i ← inst.to_u64 t
+    let i0 ← inst.to_u64 t0
+    i + i0
+
+/- Trait implementation: [traits::Tuple2::{3}] -/
+def Tuple2.ToU64Inst (A : Type) (inst : ToU64 A) : ToU64 (A × A) := {
+  to_u64 := Tuple2.to_u64 A inst
+}
+
+/- [traits::f]: forward function -/
+def f (T : Type) (inst : ToU64 T) (x : (T × T)) : Result U64 :=
+  Tuple2.to_u64 T inst x
+
+/- [traits::g]: forward function -/
+def g (T : Type) (inst : ToU64 (T × T)) (x : (T × T)) : Result U64 :=
+  inst.to_u64 x
+
+/- [traits::h0]: forward function -/
+def h0 (x : U64) : Result U64 :=
+  u64.to_u64 x
+
+/- [traits::Wrapper] -/
+structure Wrapper (T : Type) where
+  x : T
+
+/- [traits::Wrapper::{4}::to_u64]: forward function -/
+def Wrapper.to_u64
+  (T : Type) (inst : ToU64 T) (self : Wrapper T) : Result U64 :=
+  inst.to_u64 self.x
+
+/- Trait implementation: [traits::Wrapper::{4}] -/
+def Wrapper.ToU64Inst (T : Type) (inst : ToU64 T) : ToU64 (Wrapper T) := {
+  to_u64 := Wrapper.to_u64 T inst
+}
+
+/- [traits::h1]: forward function -/
+def h1 (x : Wrapper U64) : Result U64 :=
+  Wrapper.to_u64 U64 u64.ToU64Inst x
+
+/- [traits::h2]: forward function -/
+def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 :=
+  Wrapper.to_u64 T inst x
+
+/- Trait declaration: [traits::ToType] -/
+structure ToType (Self T : Type) where
+  to_type : Self → Result T
+
+/- [traits::u64::{5}::to_type]: forward function -/
+def u64.to_type (self : U64) : Result Bool :=
+  Result.ret (self > 0#u64)
+
+/- Trait implementation: [traits::u64::{5}] -/
+def u64.ToTypeInst : ToType U64 Bool := {
+  to_type := u64.to_type
+}
+
+/- Trait declaration: [traits::OfType] -/
+structure OfType (Self : Type) where
+  of_type : forall (T : Type) (inst : ToType T Self), T → Result Self
+
+/- [traits::h3]: forward function -/
+def h3
+  (T1 T2 : Type) (inst : OfType T1) (inst0 : ToType T2 T1) (y : T2) :
+  Result T1
+  :=
+  inst.of_type T2 inst0 y
+
+/- Trait declaration: [traits::OfTypeBis] -/
+structure OfTypeBis (Self T : Type) where
+  parent_clause_0 : ToType T Self
+  of_type : T → Result Self
+
+/- [traits::h4]: forward function -/
+def h4
+  (T1 T2 : Type) (inst : OfTypeBis T1 T2) (inst0 : ToType T2 T1) (y : T2) :
+  Result T1
+  :=
+  inst.of_type y
+
+/- [traits::TestType] -/
+structure TestType (T : Type) where
+  _0 : T
+
+/- [traits::TestType::{6}::test::TestType1] -/
+structure TestType.test.TestType1 where
+  _0 : U64
+
+/- Trait declaration: [traits::TestType::{6}::test::TestTrait] -/
+structure TestType.test.TestTrait (Self : Type) where
+  test : Self → Result Bool
+
+/- [traits::TestType::{6}::test::TestType1::{0}::test]: forward function -/
+def TestType.test.TestType1.test
+  (self : TestType.test.TestType1) : Result Bool :=
+  Result.ret (self._0 > 1#u64)
+
+/- Trait implementation: [traits::TestType::{6}::test::TestType1::{0}] -/
+def TestType.test.TestType1.TestTypetestTestTraitInst : TestType.test.TestTrait
+  TestType.test.TestType1 := {
+  test := TestType.test.TestType1.test
+}
+
+/- [traits::TestType::{6}::test]: forward function -/
+def TestType.test
+  (T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
+  do
+    let x0 ← inst.to_u64 x
+    if x0 > 0#u64
+    then TestType.test.TestType1.test { _0 := 0#u64 }
+    else Result.ret false
+
+/- [traits::BoolWrapper] -/
+structure BoolWrapper where
+  _0 : Bool
+
+/- [traits::BoolWrapper::{7}::to_type]: forward function -/
+def BoolWrapper.to_type
+  (T : Type) (inst : ToType Bool T) (self : BoolWrapper) : Result T :=
+  inst.to_type self._0
+
+/- Trait implementation: [traits::BoolWrapper::{7}] -/
+def BoolWrapper.ToTypeInst (T : Type) (inst : ToType Bool T) : ToType
+  BoolWrapper T := {
+  to_type := BoolWrapper.to_type T inst
+}
+
+/- [traits::WithConstTy::LEN2] -/
+def with_const_ty_len2_body : Result Usize := Result.ret 32#usize
+def with_const_ty_len2_c : Usize :=
+  eval_global with_const_ty_len2_body (by simp)
+
+/- Trait declaration: [traits::WithConstTy] -/
+structure WithConstTy (Self : Type) (LEN : Usize) where
+  LEN1 : Usize
+  LEN2 : Usize
+  V : Type
+  W : Type
+  W_clause_0 : ToU64 W
+  f : W → Array U8 LEN → Result W
+
+/- [traits::Bool::{8}::LEN1] -/
+def bool_len1_body : Result Usize := Result.ret 12#usize
+def bool_len1_c : Usize := eval_global bool_len1_body (by simp)
+
+/- [traits::Bool::{8}::f]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
+  Result.ret i
+
+/- Trait implementation: [traits::Bool::{8}] -/
+def Bool.WithConstTyInst : WithConstTy Bool 32#usize := {
+  LEN1 := bool_len1_c
+  LEN2 := with_const_ty_len2_c
+  V := U8
+  W := U64
+  W_clause_0 := u64.ToU64Inst
+  f := Bool.f
+}
+
+/- [traits::use_with_const_ty1]: forward function -/
+def use_with_const_ty1
+  (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) : Result Usize :=
+  let i := inst.LEN1
+  Result.ret i
+
+/- [traits::use_with_const_ty2]: forward function -/
+def use_with_const_ty2
+  (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (w : inst.W) :
+  Result Unit
+  :=
+  Result.ret ()
+
+/- [traits::use_with_const_ty3]: forward function -/
+def use_with_const_ty3
+  (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (x : inst.W) :
+  Result U64
+  :=
+  inst.W_clause_0.to_u64 x
+
+/- [traits::test_where1]: forward function -/
+def test_where1 (T : Type) (_x : T) : Result Unit :=
+  Result.ret ()
+
+/- [traits::test_where2]: forward function -/
+def test_where2
+  (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit :=
+  Result.ret ()
+
+/- [alloc::string::String] -/
+axiom alloc.string.String : Type
+
+/- Trait declaration: [traits::ParentTrait0] -/
+structure ParentTrait0 (Self : Type) where
+  W : Type
+  get_name : Self → Result alloc.string.String
+  get_w : Self → Result W
+
+/- Trait declaration: [traits::ParentTrait1] -/
+structure ParentTrait1 (Self : Type) where
+
+/- Trait declaration: [traits::ChildTrait] -/
+structure ChildTrait (Self : Type) where
+  parent_clause_0 : ParentTrait0 Self
+  parent_clause_1 : ParentTrait1 Self
+
+/- [traits::test_child_trait1]: forward function -/
+def test_child_trait1
+  (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String :=
+  inst.parent_clause_0.get_name x
+
+/- [traits::test_child_trait2]: forward function -/
+def test_child_trait2
+  (T : Type) (inst : ChildTrait T) (x : T) : Result inst.parent_clause_0.W :=
+  inst.parent_clause_0.get_w x
+
+/- [traits::order1]: forward function -/
+def order1
+  (T U : Type) (inst : ParentTrait0 T) (inst0 : ParentTrait0 U) :
+  Result Unit
+  :=
+  Result.ret ()
+
+/- Trait declaration: [traits::ChildTrait1] -/
+structure ChildTrait1 (Self : Type) where
+  parent_clause_0 : ParentTrait1 Self
+
+/- Trait implementation: [traits::usize::{9}] -/
+def usize.ParentTrait1Inst : ParentTrait1 Usize := {
+}
+
+/- Trait implementation: [traits::usize::{10}] -/
+def usize.ChildTrait1Inst : ChildTrait1 Usize := {
+  parent_clause_0 := usize.ParentTrait1Inst
+}
+
+/- Trait declaration: [traits::Iterator] -/
+structure Iterator (Self : Type) where
+  Item : Type
+
+/- Trait declaration: [traits::IntoIterator] -/
+structure IntoIterator (Self : Type) where
+  Item : Type
+  IntoIter : Type
+  IntoIter_clause_0 : Iterator IntoIter
+  into_iter : Self → Result IntoIter
+
+/- Trait declaration: [traits::FromResidual] -/
+structure FromResidual (Self T : Type) where
+
+/- Trait declaration: [traits::Try] -/
+structure Try (Self : Type) where
+  parent_clause_0 : FromResidual Self Residual
+  Residual : Type
+
+/- Trait declaration: [traits::CFnOnce] -/
+structure CFnOnce (Self Args : Type) where
+  Output : Type
+  call_once : Self → Args → Result Output
+
+/- Trait declaration: [traits::CFnMut] -/
+structure CFnMut (Self Args : Type) where
+  parent_clause_0 : CFnOnce Self Args
+  call_mut : Self → Args → Result parent_clause_0.Output
+  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
+
+/- Trait declaration: [traits::CFn] -/
+structure CFn (Self Args : Type) where
+  parent_clause_0 : CFnMut Self Args
+  call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output
+
+/- Trait declaration: [core::ops::function::FnOnce] -/
+structure core.ops.function.FnOnce (Self Args : Type) where
+  Output : Type
+  call_once : Self → Args → Result Output
+
+/- Trait declaration: [core::ops::function::FnMut] -/
+structure core.ops.function.FnMut (Self Args : Type) where
+  parent_clause_0 : core.ops.function.FnOnce Self Args
+  call_mut : Self → Args → Result parent_clause_0.Output
+  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
+
+/- Trait declaration: [core::ops::function::Fn] -/
+structure core.ops.function.Fn (Self Args : Type) where
+  parent_clause_0 : core.ops.function.FnMut Self Args
+  call : Self → Args → Result parent_clause_0.parent_clause_0.Output
+
+/- [traits::map_option]: forward function -/
+def map_option
+  (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) :
+  Result (Option T)
+  :=
+  match x with
+  | none => Result.ret none
+  | some x0 => do
+                 let t ← inst.call f0 x0
+                 Result.ret (some t)
+
+/- Trait declaration: [traits::WithTarget] -/
+structure WithTarget (Self : Type) where
+  Target : Type
+
+/- Trait declaration: [traits::ParentTrait2] -/
+structure ParentTrait2 (Self : Type) where
+  U : Type
+  U_clause_0 : WithTarget U
+
+/- Trait declaration: [traits::ChildTrait2] -/
+structure ChildTrait2 (Self : Type) where
+  parent_clause_0 : ParentTrait2 Self
+  convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target
+
+/- Trait implementation: [traits::u32::{11}] -/
+def u32.WithTargetInst : WithTarget U32 := {
+  Target := U32
+}
+
+/- Trait implementation: [traits::u32::{12}] -/
+def u32.ParentTrait2Inst : ParentTrait2 U32 := {
+  U := U32
+  U_clause_0 := u32.WithTargetInst
+}
+
+/- [traits::u32::{13}::convert]: forward function -/
+def u32.convert (x : U32) : Result U32 :=
+  Result.ret x
+
+/- Trait implementation: [traits::u32::{13}] -/
+def u32.ChildTrait2Inst : ChildTrait2 U32 := {
+  parent_clause_0 := u32.ParentTrait2Inst
+  convert := u32.convert
+}
+
+/- [traits::incr_u32]: forward function -/
+def incr_u32 (x : U32) : Result U32 :=
+  x + 1#u32
+
+end traits
diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean
deleted file mode 100644
index 8d423280..00000000
--- a/tests/lean/Traits/Funs.lean
+++ /dev/null
@@ -1,275 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [traits]: function definitions
-import Base
-import Traits.Types
-open Primitives
-
-namespace traits
-
-/- [traits::Bool::{0}::get_bool]: forward function -/
-def Bool.get_bool (self : Bool) : Result Bool :=
-  Result.ret self
-
-/- Trait implementation: [traits::Bool::{0}] -/
-def Bool.BoolTraitInst : BoolTrait Bool := {
-  get_bool := Bool.get_bool
-}
-
-/- [traits::BoolTrait::ret_true]: forward function -/
-def BoolTrait.ret_true
-  {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=
-  Result.ret true
-
-/- [traits::test_bool_trait_bool]: forward function -/
-def test_bool_trait_bool (x : Bool) : Result Bool :=
-  do
-    let b ← Bool.get_bool x
-    if b
-    then BoolTrait.ret_true Bool.BoolTraitInst x
-    else Result.ret false
-
-/- [traits::Option::{1}::get_bool]: forward function -/
-def Option.get_bool (T : Type) (self : Option T) : Result Bool :=
-  match self with
-  | none => Result.ret false
-  | some t => Result.ret true
-
-/- Trait implementation: [traits::Option::{1}] -/
-def Option.BoolTraitInst (T : Type) : BoolTrait (Option T) := {
-  get_bool := Option.get_bool T
-}
-
-/- [traits::test_bool_trait_option]: forward function -/
-def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
-  do
-    let b ← Option.get_bool T x
-    if b
-    then BoolTrait.ret_true (Option.BoolTraitInst T) x
-    else Result.ret false
-
-/- [traits::test_bool_trait]: forward function -/
-def test_bool_trait (T : Type) (inst : BoolTrait T) (x : T) : Result Bool :=
-  inst.get_bool x
-
-/- [traits::u64::{2}::to_u64]: forward function -/
-def u64.to_u64 (self : U64) : Result U64 :=
-  Result.ret self
-
-/- Trait implementation: [traits::u64::{2}] -/
-def u64.ToU64Inst : ToU64 U64 := {
-  to_u64 := u64.to_u64
-}
-
-/- [traits::Tuple2::{3}::to_u64]: forward function -/
-def Tuple2.to_u64 (A : Type) (inst : ToU64 A) (self : (A × A)) : Result U64 :=
-  do
-    let (t, t0) := self
-    let i ← inst.to_u64 t
-    let i0 ← inst.to_u64 t0
-    i + i0
-
-/- Trait implementation: [traits::Tuple2::{3}] -/
-def Tuple2.ToU64Inst (A : Type) (inst : ToU64 A) : ToU64 (A × A) := {
-  to_u64 := Tuple2.to_u64 A inst
-}
-
-/- [traits::f]: forward function -/
-def f (T : Type) (inst : ToU64 T) (x : (T × T)) : Result U64 :=
-  Tuple2.to_u64 T inst x
-
-/- [traits::g]: forward function -/
-def g (T : Type) (inst : ToU64 (T × T)) (x : (T × T)) : Result U64 :=
-  inst.to_u64 x
-
-/- [traits::h0]: forward function -/
-def h0 (x : U64) : Result U64 :=
-  u64.to_u64 x
-
-/- [traits::Wrapper::{4}::to_u64]: forward function -/
-def Wrapper.to_u64
-  (T : Type) (inst : ToU64 T) (self : Wrapper T) : Result U64 :=
-  inst.to_u64 self.x
-
-/- Trait implementation: [traits::Wrapper::{4}] -/
-def Wrapper.ToU64Inst (T : Type) (inst : ToU64 T) : ToU64 (Wrapper T) := {
-  to_u64 := Wrapper.to_u64 T inst
-}
-
-/- [traits::h1]: forward function -/
-def h1 (x : Wrapper U64) : Result U64 :=
-  Wrapper.to_u64 U64 u64.ToU64Inst x
-
-/- [traits::h2]: forward function -/
-def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 :=
-  Wrapper.to_u64 T inst x
-
-/- [traits::u64::{5}::to_type]: forward function -/
-def u64.to_type (self : U64) : Result Bool :=
-  Result.ret (self > 0#u64)
-
-/- Trait implementation: [traits::u64::{5}] -/
-def u64.ToTypeInst : ToType U64 Bool := {
-  to_type := u64.to_type
-}
-
-/- [traits::h3]: forward function -/
-def h3
-  (T1 T2 : Type) (inst : OfType T1) (inst0 : ToType T2 T1) (y : T2) :
-  Result T1
-  :=
-  inst.of_type T2 inst0 y
-
-/- [traits::h4]: forward function -/
-def h4
-  (T1 T2 : Type) (inst : OfTypeBis T1 T2) (inst0 : ToType T2 T1) (y : T2) :
-  Result T1
-  :=
-  inst.of_type y
-
-/- [traits::TestType::{6}::test::TestType1::{0}::test]: forward function -/
-def TestType.test.TestType1.test
-  (self : TestType.test.TestType1) : Result Bool :=
-  Result.ret (self._0 > 1#u64)
-
-/- Trait implementation: [traits::TestType::{6}::test::TestType1::{0}] -/
-def TestType.test.TestType1.TestTypetestTestTraitInst : TestType.test.TestTrait
-  TestType.test.TestType1 := {
-  test := TestType.test.TestType1.test
-}
-
-/- [traits::TestType::{6}::test]: forward function -/
-def TestType.test
-  (T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
-  do
-    let x0 ← inst.to_u64 x
-    if x0 > 0#u64
-    then TestType.test.TestType1.test { _0 := 0#u64 }
-    else Result.ret false
-
-/- [traits::BoolWrapper::{7}::to_type]: forward function -/
-def BoolWrapper.to_type
-  (T : Type) (inst : ToType Bool T) (self : BoolWrapper) : Result T :=
-  inst.to_type self._0
-
-/- Trait implementation: [traits::BoolWrapper::{7}] -/
-def BoolWrapper.ToTypeInst (T : Type) (inst : ToType Bool T) : ToType
-  BoolWrapper T := {
-  to_type := BoolWrapper.to_type T inst
-}
-
-/- [traits::WithConstTy::LEN2] -/
-def with_const_ty_len2_body : Result Usize := Result.ret 32#usize
-def with_const_ty_len2_c : Usize :=
-  eval_global with_const_ty_len2_body (by simp)
-
-/- [traits::Bool::{8}::LEN1] -/
-def bool_len1_body : Result Usize := Result.ret 12#usize
-def bool_len1_c : Usize := eval_global bool_len1_body (by simp)
-
-/- [traits::Bool::{8}::f]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
-def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
-  Result.ret i
-
-/- Trait implementation: [traits::Bool::{8}] -/
-def Bool.WithConstTyInst : WithConstTy Bool 32#usize := {
-  LEN1 := bool_len1_c
-  LEN2 := with_const_ty_len2_c
-  V := U8
-  W := U64
-  W_clause_0 := u64.ToU64Inst
-  f := Bool.f
-}
-
-/- [traits::use_with_const_ty1]: forward function -/
-def use_with_const_ty1
-  (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) : Result Usize :=
-  let i := inst.LEN1
-  Result.ret i
-
-/- [traits::use_with_const_ty2]: forward function -/
-def use_with_const_ty2
-  (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (w : inst.W) :
-  Result Unit
-  :=
-  Result.ret ()
-
-/- [traits::use_with_const_ty3]: forward function -/
-def use_with_const_ty3
-  (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (x : inst.W) :
-  Result U64
-  :=
-  inst.W_clause_0.to_u64 x
-
-/- [traits::test_where1]: forward function -/
-def test_where1 (T : Type) (_x : T) : Result Unit :=
-  Result.ret ()
-
-/- [traits::test_where2]: forward function -/
-def test_where2
-  (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit :=
-  Result.ret ()
-
-/- [traits::test_child_trait1]: forward function -/
-def test_child_trait1
-  (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String :=
-  inst.parent_clause_0.get_name x
-
-/- [traits::test_child_trait2]: forward function -/
-def test_child_trait2
-  (T : Type) (inst : ChildTrait T) (x : T) : Result inst.parent_clause_0.W :=
-  inst.parent_clause_0.get_w x
-
-/- [traits::order1]: forward function -/
-def order1
-  (T U : Type) (inst : ParentTrait0 T) (inst0 : ParentTrait0 U) :
-  Result Unit
-  :=
-  Result.ret ()
-
-/- Trait implementation: [traits::usize::{9}] -/
-def usize.ParentTrait1Inst : ParentTrait1 Usize := {
-}
-
-/- Trait implementation: [traits::usize::{10}] -/
-def usize.ChildTrait1Inst : ChildTrait1 Usize := {
-  parent_clause_0 := usize.ParentTrait1Inst
-}
-
-/- [traits::map_option]: forward function -/
-def map_option
-  (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) :
-  Result (Option T)
-  :=
-  match x with
-  | none => Result.ret none
-  | some x0 => do
-                 let t ← inst.call f0 x0
-                 Result.ret (some t)
-
-/- Trait implementation: [traits::u32::{11}] -/
-def u32.WithTargetInst : WithTarget U32 := {
-  Target := U32
-}
-
-/- Trait implementation: [traits::u32::{12}] -/
-def u32.ParentTrait2Inst : ParentTrait2 U32 := {
-  U := U32
-  U_clause_0 := u32.WithTargetInst
-}
-
-/- [traits::u32::{13}::convert]: forward function -/
-def u32.convert (x : U32) : Result U32 :=
-  Result.ret x
-
-/- Trait implementation: [traits::u32::{13}] -/
-def u32.ChildTrait2Inst : ChildTrait2 U32 := {
-  parent_clause_0 := u32.ParentTrait2Inst
-  convert := u32.convert
-}
-
-/- [traits::incr_u32]: forward function -/
-def incr_u32 (x : U32) : Result U32 :=
-  x + 1#u32
-
-end traits
diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean
deleted file mode 100644
index 4c5dd874..00000000
--- a/tests/lean/Traits/Types.lean
+++ /dev/null
@@ -1,144 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [traits]: type definitions
-import Base
-open Primitives
-
-namespace traits
-
-/- Trait declaration: [traits::BoolTrait] -/
-structure BoolTrait (Self : Type) where
-  get_bool : Self → Result Bool
-
-/- Trait declaration: [traits::ToU64] -/
-structure ToU64 (Self : Type) where
-  to_u64 : Self → Result U64
-
-/- [traits::Wrapper] -/
-structure Wrapper (T : Type) where
-  x : T
-
-/- Trait declaration: [traits::ToType] -/
-structure ToType (Self T : Type) where
-  to_type : Self → Result T
-
-/- Trait declaration: [traits::OfType] -/
-structure OfType (Self : Type) where
-  of_type : forall (T : Type) (inst : ToType T Self), T → Result Self
-
-/- Trait declaration: [traits::OfTypeBis] -/
-structure OfTypeBis (Self T : Type) where
-  parent_clause_0 : ToType T Self
-  of_type : T → Result Self
-
-/- [traits::TestType] -/
-structure TestType (T : Type) where
-  _0 : T
-
-/- [traits::TestType::{6}::test::TestType1] -/
-structure TestType.test.TestType1 where
-  _0 : U64
-
-/- Trait declaration: [traits::TestType::{6}::test::TestTrait] -/
-structure TestType.test.TestTrait (Self : Type) where
-  test : Self → Result Bool
-
-/- [traits::BoolWrapper] -/
-structure BoolWrapper where
-  _0 : Bool
-
-/- Trait declaration: [traits::WithConstTy] -/
-structure WithConstTy (Self : Type) (LEN : Usize) where
-  LEN1 : Usize
-  LEN2 : Usize
-  V : Type
-  W : Type
-  W_clause_0 : ToU64 W
-  f : W → Array U8 LEN → Result W
-
-/- [alloc::string::String] -/
-axiom alloc.string.String : Type
-
-/- Trait declaration: [traits::ParentTrait0] -/
-structure ParentTrait0 (Self : Type) where
-  W : Type
-  get_name : Self → Result alloc.string.String
-  get_w : Self → Result W
-
-/- Trait declaration: [traits::ParentTrait1] -/
-structure ParentTrait1 (Self : Type) where
-
-/- Trait declaration: [traits::ChildTrait] -/
-structure ChildTrait (Self : Type) where
-  parent_clause_0 : ParentTrait0 Self
-  parent_clause_1 : ParentTrait1 Self
-
-/- Trait declaration: [traits::ChildTrait1] -/
-structure ChildTrait1 (Self : Type) where
-  parent_clause_0 : ParentTrait1 Self
-
-/- Trait declaration: [traits::Iterator] -/
-structure Iterator (Self : Type) where
-  Item : Type
-
-/- Trait declaration: [traits::IntoIterator] -/
-structure IntoIterator (Self : Type) where
-  Item : Type
-  IntoIter : Type
-  IntoIter_clause_0 : Iterator IntoIter
-  into_iter : Self → Result IntoIter
-
-/- Trait declaration: [traits::FromResidual] -/
-structure FromResidual (Self T : Type) where
-
-/- Trait declaration: [traits::Try] -/
-structure Try (Self : Type) where
-  parent_clause_0 : FromResidual Self Residual
-  Residual : Type
-
-/- Trait declaration: [traits::CFnOnce] -/
-structure CFnOnce (Self Args : Type) where
-  Output : Type
-  call_once : Self → Args → Result Output
-
-/- Trait declaration: [traits::CFnMut] -/
-structure CFnMut (Self Args : Type) where
-  parent_clause_0 : CFnOnce Self Args
-  call_mut : Self → Args → Result parent_clause_0.Output
-  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
-
-/- Trait declaration: [traits::CFn] -/
-structure CFn (Self Args : Type) where
-  parent_clause_0 : CFnMut Self Args
-  call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output
-
-/- Trait declaration: [core::ops::function::FnOnce] -/
-structure core.ops.function.FnOnce (Self Args : Type) where
-  Output : Type
-  call_once : Self → Args → Result Output
-
-/- Trait declaration: [core::ops::function::FnMut] -/
-structure core.ops.function.FnMut (Self Args : Type) where
-  parent_clause_0 : core.ops.function.FnOnce Self Args
-  call_mut : Self → Args → Result parent_clause_0.Output
-  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
-
-/- Trait declaration: [core::ops::function::Fn] -/
-structure core.ops.function.Fn (Self Args : Type) where
-  parent_clause_0 : core.ops.function.FnMut Self Args
-  call : Self → Args → Result parent_clause_0.parent_clause_0.Output
-
-/- Trait declaration: [traits::WithTarget] -/
-structure WithTarget (Self : Type) where
-  Target : Type
-
-/- Trait declaration: [traits::ParentTrait2] -/
-structure ParentTrait2 (Self : Type) where
-  U : Type
-  U_clause_0 : WithTarget U
-
-/- Trait declaration: [traits::ChildTrait2] -/
-structure ChildTrait2 (Self : Type) where
-  parent_clause_0 : ParentTrait2 Self
-  convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target
-
-end traits
-- 
cgit v1.3.1