clippy: Fix single_char_add_str

rr_frontend/.cargo/config.toml

@@ -81,7 +81,6 @@ rustflags = [
 
     # clippy::style
     "-Aclippy::new_without_default",
-    "-Aclippy::single_char_add_str",
     "-Aclippy::single_component_path_imports",
     "-Aclippy::single_match",
     "-Aclippy::toplevel_ref_arg",

rr_frontend/radium/src/code.rs

@@ -613,9 +613,9 @@ impl Stmt {
 
                 let mut fmt_targets = String::with_capacity(100);
 
-                fmt_targets.push_str("[");
+                fmt_targets.push('[');
                 push_str_list!(fmt_targets, bs, "; ", |tgt| tgt.caesium_fmt(0));
-                fmt_targets.push_str("]");
+                fmt_targets.push(']');
 
                 let fmt_default = def.caesium_fmt(0);
 
@@ -740,7 +740,7 @@ fn make_map_string(sep0: &str, sep: &str, els: Vec<(String, String)>) -> String
         out.push_str(format!("<[{sep}\"{}\" :={}{}{}]>%E $", key, sep0, value, sep).as_str());
     }
     out.push_str(sep);
-    out.push_str("∅");
+    out.push('∅');
     out
 }
 
@@ -749,7 +749,7 @@ fn make_lft_map_string(els: Vec<(String, String)>) -> String {
     for (key, value) in &els {
         out.push_str(format!("named_lft_update \"{}\" {} $ ", key, value).as_str());
     }
-    out.push_str("∅");
+    out.push('∅');
     out
 }
 
@@ -761,7 +761,7 @@ impl FunctionCode {
         let format_stack_layout = |layout: std::slice::Iter<'_, (String, SynType)>| {
             let mut formatted_args: String = String::with_capacity(100);
 
-            formatted_args.push_str("[");
+            formatted_args.push('[');
 
             push_str_list!(formatted_args, layout, "; ", |(ref name, ref st)| {
                 let ly = st.layout_term(&[]); //should be closed already
@@ -1124,7 +1124,7 @@ impl<'def> Function<'def> {
                 if p_count > 1 {
                     ip_params.push_str(" ]");
                 }
-                ip_params.push_str(" ");
+                ip_params.push(' ');
                 p_count += 1;
                 ip_params.push_str(format!("{}", n).as_str());
             }
@@ -1138,7 +1138,7 @@ impl<'def> Function<'def> {
         } else {
             // no params, but still need to provide something to catch the unit
             // (and no empty intropatterns are allowed)
-            ip_params.push_str("?");
+            ip_params.push('?');
         }
 
         // generate intro pattern for lifetimes

rr_frontend/radium/src/specs.rs

@@ -1299,7 +1299,7 @@ impl<'def> AbstractVariant<'def> {
             typarams.push(format!("({} : syn_type)", names.syn_type));
             typarams_use.push(format!("{}", names.syn_type));
         }
-        out.push_str("\n");
+        out.push('\n');
 
         write!(out, "{}", self.generate_coq_sls_def_core(&typarams, &typarams_use)).unwrap();
 
@@ -1313,7 +1313,7 @@ impl<'def> AbstractVariant<'def> {
 
         out.push_str(&format!("struct_t {} +[", CoqAppTerm::new(&self.sls_def_name, sls_app)));
         push_str_list!(out, &self.subst_fields, ";", |(_, ty)| ty.to_string());
-        out.push_str("]");
+        out.push(']');
 
         out
     }
@@ -1389,7 +1389,7 @@ impl<'def> AbstractVariant<'def> {
             }
             out.push_str(".\n");
         }
-        out.push_str("\n");
+        out.push('\n');
 
         // write coq parameters
         let (context_names, dep_sigma) = format_extra_context_items(extra_context, &mut out).unwrap();
@@ -1895,7 +1895,7 @@ impl<'def> AbstractEnum<'def> {
 
         out.push_str(&format!("Section {}.\n", self.els_def_name));
         out.push_str(&format!("{indent}Context `{{!refinedrustGS Σ}}.\n"));
-        out.push_str("\n");
+        out.push('\n');
 
         // add syntype parameters
         let mut typarams = Vec::new();
@@ -2093,7 +2093,7 @@ impl<'def> AbstractEnum<'def> {
             }
             out.push_str(".\n");
         }
-        out.push_str("\n");
+        out.push('\n');
 
         let rt_params: Vec<_> = self.ty_params.iter().map(|x| x.refinement_type.clone()).collect();
 
@@ -2661,7 +2661,7 @@ impl<'def> FunctionSpec<'def> {
 
         out.push_str("λ ϝ, [");
         push_str_list!(out, &self.elctx, ", ", |(ref lft1, ref lft2)| format!("({lft1}, {lft2})"));
-        out.push_str("]");
+        out.push(']');
 
         out
     }
@@ -2699,8 +2699,8 @@ impl<'def> FunctionSpec<'def> {
         let mut pattern = String::with_capacity(100);
         let mut types = String::with_capacity(100);
 
-        pattern.push_str("(");
-        types.push_str("(");
+        pattern.push('(');
+        types.push('(');
 
         let mut need_sep = false;
         for (name, t) in v {
@@ -2715,8 +2715,8 @@ impl<'def> FunctionSpec<'def> {
             need_sep = true;
         }
 
-        pattern.push_str(")");
-        types.push_str(")");
+        pattern.push(')');
+        types.push(')');
 
         (pattern, CoqType::Literal(types))
     }

rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs

@@ -504,7 +504,7 @@ where
         } else {
             pre_rfn.push_str("-[");
             push_str_list!(pre_rfn, pre_types.clone(), "; ", |x| format!("#({})", x.1));
-            pre_rfn.push_str("]");
+            pre_rfn.push(']');
 
             pre_tys = pre_types.iter().map(|x| x.0.clone()).collect();
         }
@@ -561,7 +561,7 @@ where
                     CapturePostRfn::ImmutOrConsume(pat) => format!("#({pat})"),
                     CapturePostRfn::Mut(pat, gvar) => format!("#(#({pat}), {gvar})"),
                 });
-                post_term.push_str("]");
+                post_term.push(']');
 
                 builder
                     .spec

rr_frontend/translation/src/type_translator.rs

@@ -876,7 +876,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
 
                 rfn.push_str("-[");
                 push_str_list!(rfn, &field_refinements, "; ", "#({})");
-                rfn.push_str("]");
+                rfn.push(']');
 
                 invariant_spec.provide_abstracted_refinement(rfn);
             }