diff --git a/charon-pin b/charon-pin
index 6c5811cf..0a69199c 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-91f411e4de52d2fb5c7a861a374a1b9676e03dd2
+821fe7c71300e00c23e47ae97de1e8dc4ac91f9d
diff --git a/flake.lock b/flake.lock
index d1092d3a..69b0f2da 100644
--- a/flake.lock
+++ b/flake.lock
@@ -12,11 +12,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1739281352,
-        "narHash": "sha256-WR6NcKcMHvjbze83pNjvsAFuB0aOO8Iat3x2wgkNeCQ=",
+        "lastModified": 1739284006,
+        "narHash": "sha256-HfvqqGbvj1ZQwRqg83IDC9Y2tIm94g/kXgV1QRCzG0Q=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "91f411e4de52d2fb5c7a861a374a1b9676e03dd2",
+        "rev": "821fe7c71300e00c23e47ae97de1e8dc4ac91f9d",
         "type": "github"
       },
       "original": {
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index 245da018..04e6395f 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -661,12 +661,33 @@ let decompose_str_borrows (f : fun_decl) : fun_decl =
   in
   { f with body }
 
+(** When a trait method has a default implementation, this becomes a `fun_decl`
+    that we may want to extract. By default, its name is `Trait::method`, which
+    for lean creates a name clash with the method name as a field in the trait
+    struct. We therefore rename these function items to avoid the name clash.
+ *)
+let rename_default_methods (def : fun_decl) : fun_decl =
+  match def.kind with
+  | TraitDeclItem (_, _, true) ->
+      let name = def.item_meta.name in
+      let rev_name = List.rev name in
+      let method_name = List.hd rev_name in
+      let name =
+        List.rev
+          (method_name
+          :: PeIdent ("default", Disambiguator.zero)
+          :: List.tl rev_name)
+      in
+      { def with item_meta = { def.item_meta with name } }
+  | _ -> def
+
 let apply_passes (crate : crate) : crate =
   let function_passes =
     [
       remove_loop_breaks crate;
       remove_shallow_borrows crate;
       decompose_str_borrows;
+      rename_default_methods;
     ]
   in
   (* Attempt to apply a pass: if it fails we replace the body by [None] *)
diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml
index 4a2fd0a8..827abdd2 100644
--- a/src/extract/Extract.ml
+++ b/src/extract/Extract.ml
@@ -507,46 +507,24 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
       *)
       (match fun_id with
       | FromLlbc (TraitMethod (trait_ref, method_name, _fun_decl_id), lp_id) ->
-          (* We have to check whether the trait method is required or provided *)
           let trait_decl_id = trait_ref.trait_decl_ref.trait_decl_id in
           let trait_decl =
             TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls
           in
-          let method_id =
-            PureUtils.trait_decl_get_method trait_decl method_name
-          in
-
-          if not method_id.is_provided then (
-            (* Required method *)
-            sanity_check __FILE__ __LINE__ (lp_id = None)
-              trait_decl.item_meta.span;
-            extract_trait_ref trait_decl.item_meta.span ctx fmt
-              TypeDeclId.Set.empty true trait_ref;
-            let fun_name =
-              ctx_get_trait_method span trait_ref.trait_decl_ref.trait_decl_id
-                method_name ctx
-            in
-            let add_brackets (s : string) =
-              if backend () = Coq then "(" ^ s ^ ")" else s
-            in
-            F.pp_print_string fmt ("." ^ add_brackets fun_name))
-          else
-            (* Provided method: we see it as a regular function call, and use
-               the function name *)
-            let fun_id = FromLlbc (FunId (FRegular method_id.id), lp_id) in
-            let fun_name =
-              ctx_get_function trait_decl.item_meta.span fun_id ctx
-            in
-            F.pp_print_string fmt fun_name;
-
-            (* Note that we do not need to print the generics for the trait
-               declaration: they are always implicit as they can be deduced
-               from the trait self clause.
 
-               Print the trait ref (to instantate the self clause) *)
-            F.pp_print_space fmt ();
-            extract_trait_ref trait_decl.item_meta.span ctx fmt
-              TypeDeclId.Set.empty true trait_ref
+          (* Required method *)
+          sanity_check __FILE__ __LINE__ (lp_id = None)
+            trait_decl.item_meta.span;
+          extract_trait_ref trait_decl.item_meta.span ctx fmt
+            TypeDeclId.Set.empty true trait_ref;
+          let fun_name =
+            ctx_get_trait_method span trait_ref.trait_decl_ref.trait_decl_id
+              method_name ctx
+          in
+          let add_brackets (s : string) =
+            if backend () = Coq then "(" ^ s ^ ")" else s
+          in
+          F.pp_print_string fmt ("." ^ add_brackets fun_name)
       | _ ->
           let fun_name = ctx_get_function span fun_id ctx in
           F.pp_print_string fmt fun_name);
@@ -2323,7 +2301,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
     (trait_decl : trait_decl)
     (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
     extraction_ctx =
-  let required_methods = trait_decl.required_methods in
+  let methods = trait_decl.methods in
   (* Compute the names *)
   let method_names =
     match builtin_info with
@@ -2361,7 +2339,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
         List.map
           (fun (name, bound_fn) ->
             compute_item_name name bound_fn.binder_value.fun_id)
-          required_methods
+          methods
     | Some info ->
         (* This is a builtin *)
         let funs_map = StringMap.of_list info.methods in
@@ -2371,7 +2349,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
             let info = StringMap.find item_name funs_map in
             let fun_name = info.extract_name in
             (item_name, fun_name))
-          required_methods
+          methods
   in
   (* Register the names *)
   List.fold_left
@@ -2615,9 +2593,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     Option.get
       (type_decl_kind_to_qualif decl.item_meta.span SingleNonRec (Some Struct))
   in
-  (* When checking if the trait declaration is empty: we ignore the provided
-     methods, because for now they are extracted separately *)
-  let is_empty = trait_decl_is_empty { decl with provided_methods = [] } in
+  let is_empty = trait_decl_is_empty decl in
   if backend () = FStar && not is_empty then (
     F.pp_print_string fmt "noeq";
     F.pp_print_space fmt ());
@@ -2711,7 +2687,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (* The required methods *)
     List.iter
       (fun (name, fn) -> extract_trait_decl_method_items ctx fmt decl name fn)
-      decl.required_methods;
+      decl.methods;
 
     (* Close the outer boxes for the definition *)
     if backend () <> Lean then F.pp_close_box fmt ();
@@ -2772,7 +2748,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
       in
       extract_coq_arguments_instruction ctx fmt item_name params)
     decl.parent_clauses;
-  (* The required methods *)
+  (* The  methods *)
   List.iter
     (fun (item_name, bound_fn) ->
       let explicit_info = bound_fn.binder_explicit_info in
@@ -2790,7 +2766,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
         ctx_get_trait_method decl.item_meta.span decl.def_id item_name ctx
       in
       extract_coq_arguments_instruction ctx fmt item_name params)
-    decl.required_methods;
+    decl.methods;
   (* Add a space *)
   F.pp_print_space fmt ()
 
@@ -2923,9 +2899,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   extract_trait_decl_ref impl.item_meta.span ctx fmt TypeDeclId.Set.empty false
     impl.impl_trait;
 
-  (* When checking if the trait impl is empty: we ignore the provided
-     methods, because for now they are extracted separately *)
-  let is_empty = trait_impl_is_empty { impl with provided_methods = [] } in
+  let is_empty = trait_impl_is_empty impl in
 
   F.pp_print_space fmt ();
   if is_empty && backend () = FStar then (
@@ -3011,11 +2985,11 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
         extract_trait_impl_item ctx fmt item_name ty)
       (List.combine trait_decl.parent_clauses impl.parent_trait_refs);
 
-    (* The required methods *)
+    (* The methods *)
     List.iter
       (fun (name, bound_fn) ->
         extract_trait_impl_method_items ctx fmt impl name bound_fn)
-      impl.required_methods;
+      impl.methods;
 
     (* Close the outer boxes for the definition, as well as the brackets *)
     F.pp_close_box fmt ();
diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml
index 2c3835a9..8a6edb32 100644
--- a/src/extract/ExtractBase.ml
+++ b/src/extract/ExtractBase.ml
@@ -2181,11 +2181,10 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
           with
           | None -> def.item_meta
           | Some trait_decl -> (
-              let methods =
-                trait_decl.required_methods @ trait_decl.provided_methods
-              in
               match
-                List.find_opt (fun (name, _) -> name = item_name) methods
+                List.find_opt
+                  (fun (name, _) -> name = item_name)
+                  trait_decl.methods
               with
               | None -> def.item_meta
               | Some (_, bound_fn) ->
diff --git a/src/pure/Pure.ml b/src/pure/Pure.ml
index 1e41ab0b..1afcaf17 100644
--- a/src/pure/Pure.ml
+++ b/src/pure/Pure.ml
@@ -1353,8 +1353,7 @@ type trait_decl = {
   llbc_parent_clauses : Types.trait_clause list;
   consts : (trait_item_name * ty) list;
   types : trait_item_name list;
-  required_methods : (trait_item_name * fun_decl_ref binder) list;
-  provided_methods : (trait_item_name * fun_decl_ref binder) list;
+  methods : (trait_item_name * fun_decl_ref binder) list;
 }
 [@@deriving show]
 
@@ -1378,7 +1377,6 @@ type trait_impl = {
   parent_trait_refs : trait_ref list;
   consts : (trait_item_name * global_decl_ref) list;
   types : (trait_item_name * ty) list;
-  required_methods : (trait_item_name * fun_decl_ref binder) list;
-  provided_methods : (trait_item_name * fun_decl_ref binder) list;
+  methods : (trait_item_name * fun_decl_ref binder) list;
 }
 [@@deriving show]
diff --git a/src/pure/PureUtils.ml b/src/pure/PureUtils.ml
index a4553372..ac2a515e 100644
--- a/src/pure/PureUtils.ml
+++ b/src/pure/PureUtils.ml
@@ -794,24 +794,6 @@ let rec typed_pattern_to_texpression (span : Meta.span) (pat : typed_pattern) :
   | None -> None
   | Some e -> Some { e; ty = pat.ty }
 
-type trait_decl_method_decl_id = { is_provided : bool; id : fun_decl_id }
-
-let trait_decl_get_method (trait_decl : trait_decl) (method_name : string) :
-    trait_decl_method_decl_id =
-  (* First look in the required methods *)
-  let bound_method =
-    List.find_opt (fun (s, _) -> s = method_name) trait_decl.required_methods
-  in
-  match bound_method with
-  | Some (_, bound_method) ->
-      { is_provided = false; id = bound_method.binder_value.fun_id }
-  | None ->
-      (* Must be a provided method *)
-      let _, bound_method =
-        List.find (fun (s, _) -> s = method_name) trait_decl.provided_methods
-      in
-      { is_provided = true; id = bound_method.binder_value.fun_id }
-
 let trait_decl_is_empty (trait_decl : trait_decl) : bool =
   let {
     def_id = _;
@@ -825,13 +807,11 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
     llbc_parent_clauses = _;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   } =
     trait_decl
   in
-  parent_clauses = [] && consts = [] && types = [] && required_methods = []
-  && provided_methods = []
+  parent_clauses = [] && consts = [] && types = [] && methods = []
 
 let trait_impl_is_empty (trait_impl : trait_impl) : bool =
   let {
@@ -847,13 +827,11 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool =
     parent_trait_refs;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   } =
     trait_impl
   in
-  parent_trait_refs = [] && consts = [] && types = [] && required_methods = []
-  && provided_methods = []
+  parent_trait_refs = [] && consts = [] && types = [] && methods = []
 
 (** Return true if a type declaration should be extracted as a tuple, because
     it is a non-recursive structure with unnamed fields. *)
diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml
index d8935379..bcd83ae3 100644
--- a/src/symbolic/SymbolicToPure.ml
+++ b/src/symbolic/SymbolicToPure.ml
@@ -4791,8 +4791,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     parent_clauses = llbc_parent_clauses;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   } : A.trait_decl =
     trait_decl
   in
@@ -4810,17 +4809,11 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     List.map (translate_trait_clause span) llbc_parent_clauses
   in
   let consts = List.map (fun (name, ty) -> (name, translate_ty ty)) consts in
-  let required_methods =
+  let methods =
     List.map
       (fun (name, bound_fn) ->
         (name, translate_trait_method span translate_ty bound_fn))
-      required_methods
-  in
-  let provided_methods =
-    List.map
-      (fun (name, bound_fn) ->
-        (name, translate_trait_method span translate_ty bound_fn))
-      provided_methods
+      methods
   in
   {
     def_id;
@@ -4834,8 +4827,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     llbc_parent_clauses;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   }
 
 let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
@@ -4848,8 +4840,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     parent_trait_refs;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   } =
     trait_impl
   in
@@ -4876,17 +4867,11 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
       consts
   in
   let types = List.map (fun (name, ty) -> (name, translate_ty ty)) types in
-  let required_methods =
-    List.map
-      (fun (name, bound_fn) ->
-        (name, translate_trait_method span translate_ty bound_fn))
-      required_methods
-  in
-  let provided_methods =
+  let methods =
     List.map
       (fun (name, bound_fn) ->
         (name, translate_trait_method span translate_ty bound_fn))
-      provided_methods
+      methods
   in
   {
     def_id;
@@ -4901,8 +4886,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     parent_trait_refs;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   }
 
 let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
diff --git a/tests/coq/rename_attribute/RenameAttribute.v b/tests/coq/rename_attribute/RenameAttribute.v
index 937f2ad0..c2315eb0 100644
--- a/tests/coq/rename_attribute/RenameAttribute.v
+++ b/tests/coq/rename_attribute/RenameAttribute.v
@@ -12,10 +12,12 @@ Module RenameAttribute.
     Source: 'tests/src/rename_attribute.rs', lines 8:0-18:1 *)
 Record BoolTest_t (Self : Type) := mkBoolTest_t {
   BoolTest_t_getTest : Self -> result bool;
+  BoolTest_t_retTest : Self -> result bool;
 }.
 
 Arguments mkBoolTest_t { _ }.
 Arguments BoolTest_t_getTest { _ } _.
+Arguments BoolTest_t_retTest { _ } _.
 
 (** [rename_attribute::{rename_attribute::BoolTrait for bool}::get_bool]:
     Source: 'tests/src/rename_attribute.rs', lines 22:4-24:5 *)
@@ -31,6 +33,7 @@ Definition boolTraitBool_retTest (self : bool) : result bool :=
     Source: 'tests/src/rename_attribute.rs', lines 21:0-25:1 *)
 Definition BoolImpl : BoolTest_t bool := {|
   BoolTest_t_getTest := boolTraitBool_getTest;
+  BoolTest_t_retTest := boolTraitBool_retTest;
 |}.
 
 (** [rename_attribute::test_bool_trait]:
@@ -97,9 +100,9 @@ Definition no_borrows_sum (n : nat) (max : u32) : result u32 :=
   no_borrows_sum_loop n max 0%u32 0%u32
 .
 
-(** [rename_attribute::BoolTrait::ret_true]:
+(** [rename_attribute::BoolTrait::default::ret_true]:
     Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-Definition boolTrait_retTest
+Definition boolTrait_default_retTest
   {Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool :=
   Ok true
 .
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 2e23a83d..3d9e3c3c 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -12,10 +12,12 @@ Module Traits.
     Source: 'tests/src/traits.rs', lines 3:0-11:1 *)
 Record BoolTrait_t (Self : Type) := mkBoolTrait_t {
   BoolTrait_t_get_bool : Self -> result bool;
+  BoolTrait_t_ret_true : Self -> result bool;
 }.
 
 Arguments mkBoolTrait_t { _ }.
 Arguments BoolTrait_t_get_bool { _ } _.
+Arguments BoolTrait_t_ret_true { _ } _.
 
 (** [traits::{traits::BoolTrait for bool}::get_bool]:
     Source: 'tests/src/traits.rs', lines 14:4-16:5 *)
@@ -31,6 +33,7 @@ Definition boolTraitBool_ret_true (self : bool) : result bool :=
     Source: 'tests/src/traits.rs', lines 13:0-17:1 *)
 Definition BoolTraitBool : BoolTrait_t bool := {|
   BoolTrait_t_get_bool := boolTraitBool_get_bool;
+  BoolTrait_t_ret_true := boolTraitBool_ret_true;
 |}.
 
 (** [traits::test_bool_trait_bool]:
@@ -58,6 +61,7 @@ Definition boolTraitOption_ret_true
     Source: 'tests/src/traits.rs', lines 24:0-31:1 *)
 Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {|
   BoolTrait_t_get_bool := boolTraitOption_get_bool;
+  BoolTrait_t_ret_true := boolTraitOption_ret_true;
 |}.
 
 (** [traits::test_bool_trait_option]:
@@ -701,9 +705,9 @@ Definition use_foo2
   Ok (foo_foo T traitInst)
 .
 
-(** [traits::BoolTrait::ret_true]:
+(** [traits::BoolTrait::default::ret_true]:
     Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
-Definition boolTrait_ret_true
+Definition boolTrait_default_ret_true
   {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool :=
   Ok true
 .
diff --git a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
index 8e9a6996..5075039b 100644
--- a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
+++ b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
@@ -19,7 +19,10 @@ let boolTraitBool_retTest (self : bool) : result bool =
 
 (** Trait implementation: [rename_attribute::{rename_attribute::BoolTrait for bool}]
     Source: 'tests/src/rename_attribute.rs', lines 21:0-25:1 *)
-let boolImpl : boolTest_t bool = { getTest = boolTraitBool_getTest; }
+let boolImpl : boolTest_t bool = {
+  getTest = boolTraitBool_getTest;
+  retTest = boolTraitBool_retTest;
+}
 
 (** [rename_attribute::test_bool_trait]:
     Source: 'tests/src/rename_attribute.rs', lines 28:0-30:1 *)
@@ -62,9 +65,9 @@ let rec no_borrows_sum_loop
 let no_borrows_sum (max : u32) : result u32 =
   no_borrows_sum_loop max 0 0
 
-(** [rename_attribute::BoolTrait::ret_true]:
+(** [rename_attribute::BoolTrait::default::ret_true]:
     Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-let boolTrait_retTest
+let boolTrait_default_retTest
   (#self : Type0) (self_clause : boolTest_t self) (self1 : self) :
   result bool
   =
diff --git a/tests/fstar/rename_attribute/RenameAttribute.Types.fst b/tests/fstar/rename_attribute/RenameAttribute.Types.fst
index a5408425..2dbe1d34 100644
--- a/tests/fstar/rename_attribute/RenameAttribute.Types.fst
+++ b/tests/fstar/rename_attribute/RenameAttribute.Types.fst
@@ -7,7 +7,10 @@ open Primitives
 
 (** Trait declaration: [rename_attribute::BoolTrait]
     Source: 'tests/src/rename_attribute.rs', lines 8:0-18:1 *)
-noeq type boolTest_t (self : Type0) = { getTest : self -> result bool; }
+noeq type boolTest_t (self : Type0) = {
+  getTest : self -> result bool;
+  retTest : self -> result bool;
+}
 
 (** [rename_attribute::SimpleEnum]
     Source: 'tests/src/rename_attribute.rs', lines 36:0-41:1 *)
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index e19b316b..4647ca11 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -7,7 +7,10 @@ open Primitives
 
 (** Trait declaration: [traits::BoolTrait]
     Source: 'tests/src/traits.rs', lines 3:0-11:1 *)
-noeq type boolTrait_t (self : Type0) = { get_bool : self -> result bool; }
+noeq type boolTrait_t (self : Type0) = {
+  get_bool : self -> result bool;
+  ret_true : self -> result bool;
+}
 
 (** [traits::{traits::BoolTrait for bool}::get_bool]:
     Source: 'tests/src/traits.rs', lines 14:4-16:5 *)
@@ -21,7 +24,10 @@ let boolTraitBool_ret_true (self : bool) : result bool =
 
 (** Trait implementation: [traits::{traits::BoolTrait for bool}]
     Source: 'tests/src/traits.rs', lines 13:0-17:1 *)
-let boolTraitBool : boolTrait_t bool = { get_bool = boolTraitBool_get_bool; }
+let boolTraitBool : boolTrait_t bool = {
+  get_bool = boolTraitBool_get_bool;
+  ret_true = boolTraitBool_ret_true;
+}
 
 (** [traits::test_bool_trait_bool]:
     Source: 'tests/src/traits.rs', lines 19:0-21:1 *)
@@ -43,6 +49,7 @@ let boolTraitOption_ret_true (#t : Type0) (self : option t) : result bool =
     Source: 'tests/src/traits.rs', lines 24:0-31:1 *)
 let boolTraitOption (t : Type0) : boolTrait_t (option t) = {
   get_bool = boolTraitOption_get_bool;
+  ret_true = boolTraitOption_ret_true;
 }
 
 (** [traits::test_bool_trait_option]:
@@ -524,9 +531,9 @@ let use_foo2
   =
   Ok (foo_foo t traitInst)
 
-(** [traits::BoolTrait::ret_true]:
+(** [traits::BoolTrait::default::ret_true]:
     Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
-let boolTrait_ret_true
+let boolTrait_default_ret_true
   (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) :
   result bool
   =
diff --git a/tests/lean/RenameAttribute.lean b/tests/lean/RenameAttribute.lean
index 5dffae3b..78a0f956 100644
--- a/tests/lean/RenameAttribute.lean
+++ b/tests/lean/RenameAttribute.lean
@@ -12,6 +12,7 @@ namespace rename_attribute
    Source: 'tests/src/rename_attribute.rs', lines 8:0-18:1 -/
 structure BoolTest (Self : Type) where
   getTest : Self → Result Bool
+  retTest : Self → Result Bool
 
 /- [rename_attribute::{rename_attribute::BoolTrait for bool}::get_bool]:
    Source: 'tests/src/rename_attribute.rs', lines 22:4-24:5 -/
@@ -28,6 +29,7 @@ def BoolTraitBool.retTest (self : Bool) : Result Bool :=
 @[reducible]
 def BoolImpl : BoolTest Bool := {
   getTest := BoolTraitBool.getTest
+  retTest := BoolTraitBool.retTest
 }
 
 /- [rename_attribute::test_bool_trait]:
@@ -89,9 +91,9 @@ divergent def No_borrows_sum_loop
 def No_borrows_sum (max : U32) : Result U32 :=
   No_borrows_sum_loop max 0#u32 0#u32
 
-/- [rename_attribute::BoolTrait::ret_true]:
+/- [rename_attribute::BoolTrait::default::ret_true]:
    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 -/
-def BoolTrait.retTest
+def BoolTrait.default.retTest
   {Self : Type} (self_clause : BoolTest Self) (self : Self) : Result Bool :=
   Result.ok true
 
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 81047656..87d868a0 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -12,6 +12,7 @@ namespace traits
    Source: 'tests/src/traits.rs', lines 3:0-11:1 -/
 structure BoolTrait (Self : Type) where
   get_bool : Self → Result Bool
+  ret_true : Self → Result Bool
 
 /- [traits::{traits::BoolTrait for bool}::get_bool]:
    Source: 'tests/src/traits.rs', lines 14:4-16:5 -/
@@ -28,6 +29,7 @@ def BoolTraitBool.ret_true (self : Bool) : Result Bool :=
 @[reducible]
 def BoolTraitBool : BoolTrait Bool := {
   get_bool := BoolTraitBool.get_bool
+  ret_true := BoolTraitBool.ret_true
 }
 
 /- [traits::test_bool_trait_bool]:
@@ -56,6 +58,7 @@ def BoolTraitOption.ret_true {T : Type} (self : Option T) : Result Bool :=
 @[reducible]
 def BoolTraitOption (T : Type) : BoolTrait (Option T) := {
   get_bool := BoolTraitOption.get_bool
+  ret_true := BoolTraitOption.ret_true
 }
 
 /- [traits::test_bool_trait_option]:
@@ -547,9 +550,9 @@ def use_foo2
   :=
   Result.ok (Foo.FOO T TraitInst)
 
-/- [traits::BoolTrait::ret_true]:
+/- [traits::BoolTrait::default::ret_true]:
    Source: 'tests/src/traits.rs', lines 8:4-10:5 -/
-def BoolTrait.ret_true
+def BoolTrait.default.ret_true
   {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=
   Result.ok true