Typeclasses: members with names beginning with _ do not get methods

src/tosyntax/FStarC.ToSyntax.ToSyntax.fst

@@ -3921,7 +3921,9 @@ and desugar_decl_core env (d_attrs:list S.term) (d:decl) : (env_t & sigelts) =
                    else false)
               formals
           in
-          let meths = List.filter (fun x -> not (has_no_method_attr x)) meths in
+          (* If the name begins with _, or if it has the no_method attribute, then
+           * it will not be defined. So we filter it out of the names declared by the splice. *)
+          let meths = List.filter (fun x -> not (String.index (string_of_id (ident_of_lid x)) 0 = '_') && not (has_no_method_attr x)) meths in
           let is_typed = false in
           [{ sigel = Sig_splice {is_typed; lids=meths; tac=mkclass lid};
              sigquals = [];

ulib/FStar.Tactics.Typeclasses.fst

@@ -353,12 +353,16 @@ let rec last (l : list 'a) : Tac 'a =
 
 private
 let filter_no_method_binders (bs:binders)
-  : binders
+  : Tac binders
   = let open FStar.Reflection.TermEq.Simple in
     let has_no_method_attr (b:binder) : bool =
       L.existsb (term_eq (`no_method)) b.attrs
     in
-    bs |> L.filter (fun b -> not (has_no_method_attr b))
+    bs |> Tactics.Util.filter (fun b ->
+      let nm = unseal b.ppname in
+      assume (String.length nm > 0); (* should be provided by F*? *)
+      if FStar.String.index nm 0 = '_' then false
+      else not (has_no_method_attr b))
 
 private
 let binder_set_meta (b : binder) (t : term) : binder =