diff --git a/cli/driver/src/driver.rs b/cli/driver/src/driver.rs
index 66911e338..bccfe3a96 100644
--- a/cli/driver/src/driver.rs
+++ b/cli/driver/src/driver.rs
@@ -78,15 +78,20 @@ const HAX_VANILLA_RUSTC: &str = "HAX_VANILLA_RUSTC";
 fn main() {
     setup_logging();
 
-    let options: hax_types::cli_options::Options =
-        serde_json::from_str(&std::env::var(ENV_VAR_OPTIONS_FRONTEND).expect(&format!(
-            "Cannot find environnement variable {}",
-            ENV_VAR_OPTIONS_FRONTEND
-        )))
-        .expect(&format!(
+    let options: hax_types::cli_options::Options = serde_json::from_str(
+        &std::env::var(ENV_VAR_OPTIONS_FRONTEND).unwrap_or_else(|_| {
+            panic!(
+                "Cannot find environnement variable {}",
+                ENV_VAR_OPTIONS_FRONTEND
+            )
+        }),
+    )
+    .unwrap_or_else(|_| {
+        panic!(
             "Invalid value for the environnement variable {}",
             ENV_VAR_OPTIONS_FRONTEND
-        ));
+        )
+    });
 
     let mut rustc_args: Vec<String> = std::env::args().skip(1).collect();
     // add [--sysroot] if not present
@@ -140,9 +145,7 @@ fn main() {
             adt_const_params: false,    // not useful for now
             generic_const_exprs: false, // not useful for now
             register_tool: true,
-            registered_tools: HashSet::from_iter(
-                vec![hax_lib_macros_types::HAX_TOOL.into()].into_iter(),
-            ),
+            registered_tools: HashSet::from_iter(vec![hax_lib_macros_types::HAX_TOOL.into()]),
             auto_traits: true,
             negative_impls: true,
         } - Features::detect_forking();
diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs
index 8b3d54a7e..8e0a85cf1 100644
--- a/cli/driver/src/exporter.rs
+++ b/cli/driver/src/exporter.rs
@@ -1,4 +1,3 @@
-use hax_frontend_exporter;
 use hax_frontend_exporter::state::{ExportedSpans, LocalContextS};
 use hax_frontend_exporter::SInto;
 use hax_types::cli_options::{Backend, PathOrDash, ENV_VAR_OPTIONS_FRONTEND};
@@ -19,11 +18,11 @@ use std::rc::Rc;
 
 type ThirBundle<'tcx> = (Rc<rustc_middle::thir::Thir<'tcx>>, ExprId);
 /// Generates a dummy THIR body with an error literal as first expression
-fn dummy_thir_body<'tcx>(
-    tcx: TyCtxt<'tcx>,
+fn dummy_thir_body(
+    tcx: TyCtxt<'_>,
     span: rustc_span::Span,
     guar: rustc_errors::ErrorGuaranteed,
-) -> ThirBundle<'tcx> {
+) -> ThirBundle<'_> {
     use rustc_middle::thir::*;
     let ty = tcx.mk_ty_from_kind(rustc_type_ir::TyKind::Never);
     let mut thir = Thir::new(BodyTy::Const(ty));
@@ -45,9 +44,9 @@ fn dummy_thir_body<'tcx>(
 
 /// Precompute all THIR bodies in a certain order so that we avoid
 /// stealing issues (theoretically...)
-fn precompute_local_thir_bodies<'tcx>(
-    tcx: TyCtxt<'tcx>,
-) -> std::collections::HashMap<rustc_span::def_id::LocalDefId, ThirBundle<'tcx>> {
+fn precompute_local_thir_bodies(
+    tcx: TyCtxt<'_>,
+) -> std::collections::HashMap<rustc_span::def_id::LocalDefId, ThirBundle<'_>> {
     let hir = tcx.hir();
     use rustc_hir::def::DefKind::*;
     use rustc_hir::*;
@@ -79,7 +78,7 @@ fn precompute_local_thir_bodies<'tcx>(
         .filter(|ldid| {
             match tcx.def_kind(ldid.to_def_id()) {
                 InlineConst | AnonConst => {
-                    fn is_fn<'tcx>(tcx: TyCtxt<'tcx>, did: rustc_span::def_id::DefId) -> bool {
+                    fn is_fn(tcx: TyCtxt<'_>, did: rustc_span::def_id::DefId) -> bool {
                         use rustc_hir::def::DefKind;
                         matches!(
                             tcx.def_kind(did),
diff --git a/cli/driver/src/features.rs b/cli/driver/src/features.rs
index 9d0aa3a5a..afbd0913c 100644
--- a/cli/driver/src/features.rs
+++ b/cli/driver/src/features.rs
@@ -104,7 +104,7 @@ impl Features {
         };
         let exit_code = rustc_driver::catch_with_exit_code(|| {
             rustc_driver::RunCompiler::new(
-                &rustc_args,
+                rustc_args,
                 &mut CallbacksWrapper {
                     sub: &mut callbacks,
                     options: options.clone(),
diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs
index ffcabb968..c24ddfc48 100644
--- a/cli/subcommands/src/cargo_hax.rs
+++ b/cli/subcommands/src/cargo_hax.rs
@@ -87,12 +87,8 @@ fn find_hax_engine(message_format: MessageFormat) -> process::Command {
 
     std::env::var("HAX_ENGINE_BINARY")
         .ok()
-        .map(|name| process::Command::new(name))
-        .or_else(|| {
-            which(ENGINE_BINARY_NAME)
-                .ok()
-                .map(|name| process::Command::new(name))
-        })
+        .map(process::Command::new)
+        .or_else(|| which(ENGINE_BINARY_NAME).ok().map(process::Command::new))
         .or_else(|| {
             which("node").ok().and_then(|_| {
                 if let Ok(true) = inquire::Confirm::new(&format!(
@@ -184,7 +180,7 @@ impl HaxMessage {
             }
             Self::CargoBuildFailure => {
                 let title =
-                    format!("hax: running `cargo build` was not successful, continuing anyway.");
+                    "hax: running `cargo build` was not successful, continuing anyway.".to_string();
                 eprintln!("{}", renderer.render(Level::Warning.title(&title)));
             }
             Self::WarnExperimentalBackend { backend } => {
@@ -215,14 +211,13 @@ fn run_engine(
         .stdin(std::process::Stdio::piped())
         .stdout(std::process::Stdio::piped())
         .spawn()
-        .map_err(|e| {
+        .inspect_err(|e| {
             if let std::io::ErrorKind::NotFound = e.kind() {
                 panic!(
                     "The binary [{}] was not found in your [PATH].",
                     ENGINE_BINARY_NAME
                 )
             }
-            e
         })
         .unwrap();
 
@@ -288,7 +283,7 @@ fn run_engine(
                         output.files.push(file)
                     } else {
                         let path = out_dir.join(&file.path);
-                        std::fs::create_dir_all(&path.parent().unwrap()).unwrap();
+                        std::fs::create_dir_all(path.parent().unwrap()).unwrap();
                         let mut wrote = false;
                         if fs::read_to_string(&path).as_ref().ok() != Some(&file.contents) {
                             std::fs::write(&path, file.contents).unwrap();
@@ -326,7 +321,8 @@ fn run_engine(
     if !exit_status.success() {
         HaxMessage::HaxEngineFailure {
             exit_code: exit_status.code().unwrap_or(-1),
-        };
+        }
+        .report(message_format, None);
         std::process::exit(1);
     }
 
diff --git a/engine/utils/phase-debug-webapp/src/lib.rs b/engine/utils/phase-debug-webapp/src/lib.rs
index 95719f636..598114725 100644
--- a/engine/utils/phase-debug-webapp/src/lib.rs
+++ b/engine/utils/phase-debug-webapp/src/lib.rs
@@ -32,7 +32,7 @@ pub fn run(get_json: impl Fn() -> String) {
             path if path.starts_with("/debug-hax-engine.json") => {
                 Response::from_string(get_json()).with_header(ct_utf8.clone())
             }
-            _ => Response::from_string(format!("Unknown route")).with_status_code(404),
+            _ => Response::from_string("Unknown route".to_string()).with_status_code(404),
         };
         let _ = request.respond(response);
     }
diff --git a/frontend/exporter/options/src/lib.rs b/frontend/exporter/options/src/lib.rs
index 1accf3d9e..28d0264bb 100644
--- a/frontend/exporter/options/src/lib.rs
+++ b/frontend/exporter/options/src/lib.rs
@@ -36,9 +36,8 @@ impl std::convert::From<String> for Namespace {
         Namespace {
             chunks: s
                 .split("::")
-                .into_iter()
-                .filter(|s| s.len() > 0)
-                .map(|s| NamespaceChunk::from(s))
+                .filter(|s| !s.is_empty())
+                .map(NamespaceChunk::from)
                 .collect(),
         }
     }
diff --git a/frontend/exporter/src/body.rs b/frontend/exporter/src/body.rs
index 458e241cb..8d47409cd 100644
--- a/frontend/exporter/src/body.rs
+++ b/frontend/exporter/src/body.rs
@@ -36,7 +36,7 @@ mod module {
         s: &S,
     ) -> FnDef<Body> {
         let hir_id = body_id.hir_id;
-        let ldid = hir_id.clone().owner.def_id;
+        let ldid = hir_id.owner.def_id;
 
         let (thir, expr_entrypoint) = get_thir(ldid, s);
         let s = &with_owner_id(s.base(), thir.clone(), (), ldid.to_def_id());
@@ -64,15 +64,13 @@ mod module {
     mod implementations {
         use super::*;
         impl IsBody for () {
-            fn body<'tcx, S: UnderOwnerState<'tcx>>(_did: RLocalDefId, _s: &S) -> Self {
-                ()
-            }
+            fn body<'tcx, S: UnderOwnerState<'tcx>>(_did: RLocalDefId, _s: &S) -> Self {}
         }
         impl IsBody for ThirBody {
             fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self {
                 let (thir, expr) = get_thir(did, s);
                 if *CORE_EXTRACTION_MODE {
-                    let expr = &thir.exprs[expr.clone()];
+                    let expr = &thir.exprs[expr];
                     Decorated {
                         contents: Box::new(ExprKind::Tuple { fields: vec![] }),
                         hir_id: None,
@@ -111,7 +109,7 @@ mod module {
 
     impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, Body> for rustc_hir::BodyId {
         fn sinto(&self, s: &S) -> Body {
-            body_from_id::<Body, _>(self.clone(), s)
+            body_from_id::<Body, _>(*self, s)
         }
     }
 }
diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs
index bc5bc2ebd..08ae7d9fd 100644
--- a/frontend/exporter/src/constant_utils.rs
+++ b/frontend/exporter/src/constant_utils.rs
@@ -214,9 +214,7 @@ mod rustc {
     ) -> ConstantLiteral {
         match ty.kind() {
             ty::Char => ConstantLiteral::Char(
-                char::try_from(x)
-                    .s_expect(s, "scalar_int_to_constant_literal: expected a char")
-                    .into(),
+                char::try_from(x).s_expect(s, "scalar_int_to_constant_literal: expected a char"),
             ),
             ty::Bool => ConstantLiteral::Bool(
                 x.try_to_bool()
@@ -296,7 +294,7 @@ mod rustc {
                             },
                         );
                         ConstantExprKind::Literal(ConstantLiteral::ByteStr(
-                            values.iter().copied().collect(),
+                            values.to_vec(),
                             StrStyle::Cooked,
                         ))
                     }
@@ -356,9 +354,9 @@ mod rustc {
     /// Rustc; we don't want to reflect that, instead we prefer inlining
     /// those. `is_anon_const` is used to detect such AnonConst so that we
     /// can evaluate and inline them.
-    pub(crate) fn is_anon_const<'tcx>(
+    pub(crate) fn is_anon_const(
         did: rustc_span::def_id::DefId,
-        tcx: rustc_middle::ty::TyCtxt<'tcx>,
+        tcx: rustc_middle::ty::TyCtxt<'_>,
     ) -> bool {
         matches!(
             tcx.def_path(did).data.last().map(|x| x.data),
@@ -489,7 +487,7 @@ mod rustc {
                 }
 
                 ty::ConstKind::Unevaluated(ucv) => match self.translate_uneval(s, ucv, span) {
-                    TranslateUnevalRes::EvaluatedConstant(c) => return c.sinto(s),
+                    TranslateUnevalRes::EvaluatedConstant(c) => c.sinto(s),
                     TranslateUnevalRes::GlobalName(c) => c,
                 },
                 ty::ConstKind::Value(ty, valtree) => valtree_to_constant_expr(s, valtree, ty, span),
diff --git a/frontend/exporter/src/index_vec.rs b/frontend/exporter/src/index_vec.rs
index 950af531c..8b516fc2b 100644
--- a/frontend/exporter/src/index_vec.rs
+++ b/frontend/exporter/src/index_vec.rs
@@ -35,10 +35,10 @@ impl<I: rustc_index::Idx, T: Sized> std::ops::DerefMut for IndexVec<I, T> {
 }
 
 #[cfg(feature = "rustc")]
-impl<I: rustc_index::Idx, T> Into<IndexVec<I, T>> for rustc_index::IndexVec<I, T> {
-    fn into(self) -> IndexVec<I, T> {
+impl<I: rustc_index::Idx, T> From<rustc_index::IndexVec<I, T>> for IndexVec<I, T> {
+    fn from(val: rustc_index::IndexVec<I, T>) -> Self {
         IndexVec {
-            raw: self.raw,
+            raw: val.raw,
             _marker: std::marker::PhantomData,
         }
     }
diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs
index 179c8b86c..c20fb0683 100644
--- a/frontend/exporter/src/rustc_utils.rs
+++ b/frontend/exporter/src/rustc_utils.rs
@@ -37,7 +37,7 @@ pub(crate) fn get_variant_information<'s, S: UnderOwnerState<'s>>(
     s_assert!(s, !adt_def.is_union() || *CORE_EXTRACTION_MODE);
     fn is_record<'s, I: std::iter::Iterator<Item = &'s ty::FieldDef> + Clone>(it: I) -> bool {
         it.clone()
-            .any(|field| !field.name.to_ident_string().parse::<u64>().is_ok())
+            .any(|field| field.name.to_ident_string().parse::<u64>().is_err())
     }
     let variant_def = adt_def.variant(variant_index);
     let variant = variant_def.def_id;
@@ -109,7 +109,7 @@ pub(crate) fn read_span_from_file(span: &Span) -> Result<String, ReadSpanErr> {
             let first = first.chars().skip(span.lo.col).collect();
             let last = last.chars().take(span.hi.col).collect();
             Ok(std::iter::once(first)
-                .chain(middle.into_iter().cloned())
+                .chain(middle.iter().cloned())
                 .chain(std::iter::once(last))
                 .collect::<Vec<String>>()
                 .join("\n"))
@@ -145,7 +145,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> ParamEnv<'tcx> for S {
 
 #[tracing::instrument]
 pub fn argument_span_of_mac_call(mac_call: &rustc_ast::ast::MacCall) -> rustc_span::Span {
-    (*mac_call.args).dspan.entire()
+    mac_call.args.dspan.entire()
 }
 #[tracing::instrument(skip(state))]
 pub(crate) fn raw_macro_invocation_of_span<'t, S: BaseState<'t>>(
@@ -224,7 +224,7 @@ pub(crate) fn attribute_from_scope<'tcx, S: ExprState<'tcx>>(
     let map = tcx.hir();
     let attributes = hir_id
         .map(|hir_id| map.attrs(hir_id).sinto(s))
-        .unwrap_or(vec![]);
+        .unwrap_or_default();
     (hir_id, attributes)
 }
 
@@ -247,7 +247,7 @@ pub fn inline_macro_invocations<'t, S: BaseState<'t>, Body: IsBody>(
     ids.map(|id| tcx.hir().item(id))
         .group_by(|item| SpanEq(raw_macro_invocation_of_span(item.span, s)))
         .into_iter()
-        .map(|(mac, items)| match mac.0 {
+        .flat_map(|(mac, items)| match mac.0 {
             Some((macro_ident, expn_data)) => {
                 let owner_id: rustc_hir::hir_id::OwnerId =
                     items.into_iter().map(|x| x.owner_id).next().s_unwrap(s);
@@ -267,6 +267,5 @@ pub fn inline_macro_invocations<'t, S: BaseState<'t>, Body: IsBody>(
             }
             _ => items.map(|item| item.sinto(s)).collect(),
         })
-        .flatten()
         .collect()
 }
diff --git a/frontend/exporter/src/sinto.rs b/frontend/exporter/src/sinto.rs
index dc162aa70..84342c983 100644
--- a/frontend/exporter/src/sinto.rs
+++ b/frontend/exporter/src/sinto.rs
@@ -45,7 +45,7 @@ mod test {
     pub struct Foo(usize);
     impl Foo {
         pub fn as_usize(&self) -> usize {
-            self.0.clone()
+            self.0
         }
     }
 }
@@ -76,24 +76,24 @@ impl<S, D, T: SInto<S, D>> SInto<S, D> for &T {
 }
 impl<S, D: Clone, T: SInto<S, D>> SInto<S, Vec<D>> for [T] {
     fn sinto(&self, s: &S) -> Vec<D> {
-        self.into_iter().map(|x| x.sinto(s)).collect()
+        self.iter().map(|x| x.sinto(s)).collect()
     }
 }
 impl<S, D: Clone, T: SInto<S, D>> SInto<S, Vec<D>> for Box<[T]> {
     fn sinto(&self, s: &S) -> Vec<D> {
-        (&*self).into_iter().map(|x| x.sinto(s)).collect()
+        self.into_iter().map(|x| x.sinto(s)).collect()
     }
 }
 
 impl<S, D: Clone, T: SInto<S, D>> SInto<S, Vec<D>> for Vec<T> {
     fn sinto(&self, s: &S) -> Vec<D> {
-        self.into_iter().map(|x| x.sinto(s)).collect()
+        self.iter().map(|x| x.sinto(s)).collect()
     }
 }
 #[cfg(feature = "rustc")]
 impl<S> SInto<S, Vec<u8>> for rustc_data_structures::sync::Lrc<[u8]> {
     fn sinto(&self, _s: &S) -> Vec<u8> {
-        (**self).iter().cloned().collect()
+        (**self).to_vec()
     }
 }
 
diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs
index 35c15844c..f94d04fe1 100644
--- a/frontend/exporter/src/state.rs
+++ b/frontend/exporter/src/state.rs
@@ -105,6 +105,12 @@ mod types {
         pub vars: HashMap<rustc_middle::thir::LocalVarId, String>,
     }
 
+    impl Default for LocalContextS {
+        fn default() -> Self {
+            Self::new()
+        }
+    }
+
     impl LocalContextS {
         pub fn new() -> LocalContextS {
             LocalContextS {
@@ -260,12 +266,12 @@ impl<'tcx> StateWithOwner<'tcx> {
 }
 
 /// Updates the OnwerId in a state, making sure to override `opt_def_id` in base as well.
-pub fn with_owner_id<'tcx, THIR, MIR>(
-    mut base: types::Base<'tcx>,
+pub fn with_owner_id<THIR, MIR>(
+    mut base: types::Base<'_>,
     thir: THIR,
     mir: MIR,
     owner_id: rustc_hir::def_id::DefId,
-) -> State<types::Base<'tcx>, THIR, MIR, rustc_hir::def_id::DefId, ()> {
+) -> State<types::Base<'_>, THIR, MIR, rustc_hir::def_id::DefId, ()> {
     base.opt_def_id = Some(owner_id);
     State {
         thir,
@@ -289,7 +295,7 @@ pub trait UnderBinderState<'tcx> = UnderOwnerState<'tcx> + HasBinder<'tcx>;
 pub trait ExprState<'tcx> = UnderOwnerState<'tcx> + HasThir<'tcx>;
 
 impl ImplInfos {
-    fn from<'tcx>(base: Base<'tcx>, did: rustc_hir::def_id::DefId) -> Self {
+    fn from(base: Base<'_>, did: rustc_hir::def_id::DefId) -> Self {
         let tcx = base.tcx;
         let s = &with_owner_id(base, (), (), did);
 
@@ -315,7 +321,7 @@ pub fn impl_def_ids_to_impled_types_and_bounds<'tcx, S: BaseState<'tcx>>(
 
     let def_ids = exported_def_ids.as_ref().borrow().clone();
     let with_parents = |mut did: rustc_hir::def_id::DefId| {
-        let mut acc = vec![did.clone()];
+        let mut acc = vec![did];
         while let Some(parent) = tcx.opt_parent(did) {
             did = parent;
             acc.push(did);
@@ -326,8 +332,7 @@ pub fn impl_def_ids_to_impled_types_and_bounds<'tcx, S: BaseState<'tcx>>(
     def_ids
         .iter()
         .cloned()
-        .map(with_parents)
-        .flatten()
+        .flat_map(with_parents)
         .unique()
         .filter(|&did| {
             // keep only DefIds that corresponds to implementations
diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
index 01f349f06..076aa9626 100644
--- a/frontend/exporter/src/traits.rs
+++ b/frontend/exporter/src/traits.rs
@@ -277,7 +277,7 @@ pub mod rustc {
             let y = erase_and_norm(y);
             let sx = format!("{:?}", x.kind().skip_binder());
             let sy = format!("{:?}", y.kind().skip_binder());
-            let result = sx == sy;
+
             // const DEBUG: bool = false;
             // if DEBUG && result {
             //     use crate::{Predicate, SInto};
@@ -296,7 +296,7 @@ pub mod rustc {
             //         eprintln!("sinto(y)={:#?}", ys);
             //     }
             // }
-            result
+            sx == sy
         }
 
         #[extension_traits::extension(pub trait TraitPredicateExt)]
@@ -504,7 +504,7 @@ pub mod rustc {
         warn: &impl Fn(&str),
     ) -> Result<Vec<ImplExpr<'tcx>>, String> {
         obligations
-            .into_iter()
+            .iter()
             .flat_map(|obligation| {
                 obligation.predicate.as_trait_clause().map(|trait_ref| {
                     impl_expr(
@@ -543,7 +543,7 @@ pub mod rustc {
                 generics,
             },
             Ok(ImplSource::Param(_)) => {
-                match search_clause::path_to(tcx, owner_id, param_env, tref.clone()) {
+                match search_clause::path_to(tcx, owner_id, param_env, *tref) {
                     Some((path, apred)) => {
                         let r#trait = apred.clause.to_poly_trait_ref();
                         match apred.origin {
@@ -568,9 +568,7 @@ pub mod rustc {
                 }
             }
             Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => ImplExprAtom::Dyn,
-            Ok(ImplSource::Builtin(_, _)) => ImplExprAtom::Builtin {
-                r#trait: tref.clone(),
-            },
+            Ok(ImplSource::Builtin(_, _)) => ImplExprAtom::Builtin { r#trait: *tref },
             Err(e) => {
                 let msg = format!(
                     "Could not find a clause for `{tref:?}` in the current context: `{e:?}`"
diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
index 36711b3dd..e08a0d274 100644
--- a/frontend/exporter/src/types/copied.rs
+++ b/frontend/exporter/src/types/copied.rs
@@ -21,9 +21,9 @@ impl std::hash::Hash for DefId {
 #[cfg(feature = "rustc")]
 impl<'s, S: BaseState<'s>> SInto<S, DefId> for rustc_hir::def_id::DefId {
     fn sinto(&self, s: &S) -> DefId {
-        s.base().exported_def_ids.borrow_mut().insert(self.clone());
+        s.base().exported_def_ids.borrow_mut().insert(*self);
         let tcx = s.base().tcx;
-        let def_path = tcx.def_path(self.clone());
+        let def_path = tcx.def_path(*self);
         let krate = tcx.crate_name(def_path.krate);
         DefId {
             path: def_path.data.iter().map(|x| x.sinto(s)).collect(),
@@ -226,19 +226,16 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for rustc_middle::mi
         use rustc_middle::mir::Const;
         let tcx = s.base().tcx;
         match self {
-            Const::Val(const_value, ty) => const_value_to_constant_expr(
-                s,
-                ty.clone(),
-                const_value.clone(),
-                rustc_span::DUMMY_SP,
-            ),
+            Const::Val(const_value, ty) => {
+                const_value_to_constant_expr(s, *ty, *const_value, rustc_span::DUMMY_SP)
+            }
             Const::Ty(_ty, c) => c.sinto(s),
             Const::Unevaluated(ucv, _ty) => {
                 use crate::rustc_middle::query::Key;
                 let span = tcx
                     .def_ident_span(ucv.def)
                     .unwrap_or_else(|| ucv.def.default_span(tcx));
-                if let Some(_) = ucv.promoted {
+                if ucv.promoted.is_some() {
                     self.eval_constant(s)
                         .unwrap_or_else(|| {
                             supposely_unreachable_fatal!(s, "UnevalPromotedConstant"; {self, ucv});
@@ -991,11 +988,11 @@ const _: () = {
 };
 
 #[cfg(feature = "rustc")]
-impl Into<Loc> for rustc_span::Loc {
-    fn into(self) -> Loc {
+impl From<rustc_span::Loc> for Loc {
+    fn from(val: rustc_span::Loc) -> Self {
         Loc {
-            line: self.line,
-            col: self.col_display,
+            line: val.line,
+            col: val.col_display,
         }
     }
 }
@@ -1004,8 +1001,8 @@ impl Into<Loc> for rustc_span::Loc {
 impl<'tcx, S: BaseState<'tcx>> SInto<S, Span> for rustc_span::Span {
     fn sinto(&self, s: &S) -> Span {
         let set: crate::state::ExportedSpans = s.base().exported_spans;
-        set.borrow_mut().insert(self.clone());
-        translate_span(self.clone(), s.base().tcx.sess)
+        set.borrow_mut().insert(*self);
+        translate_span(*self, s.base().tcx.sess)
     }
 }
 
@@ -1027,10 +1024,9 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, LocalIdent> for rustc_middle::thir
                 .borrow()
                 .vars
                 .get(self)
-                .clone()
                 .s_unwrap(s)
                 .to_string(),
-            id: self.clone().0.sinto(s),
+            id: self.0.sinto(s),
         }
     }
 }
@@ -1527,7 +1523,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Pat> for rustc_middle::thir::Pat<'tcx> {
             rustc_middle::thir::PatKind::Leaf { subpatterns } => match ty.kind() {
                 rustc_middle::ty::TyKind::Adt(adt_def, args) => {
                     (rustc_middle::thir::PatKind::Variant {
-                        adt_def: adt_def.clone(),
+                        adt_def: *adt_def,
                         args,
                         variant_index: rustc_target::abi::VariantIdx::from_usize(0),
                         subpatterns: subpatterns.clone(),
@@ -2082,7 +2078,7 @@ pub enum PatKind {
     #[custom_arm(
         rustc_middle::thir::PatKind::Binding {name, mode, var, ty, subpattern, is_primary} => {
             let local_ctx = gstate.base().local_ctx;
-            local_ctx.borrow_mut().vars.insert(var.clone(), name.to_string());
+            local_ctx.borrow_mut().vars.insert(*var, name.to_string());
             PatKind::Binding {
                 mode: mode.sinto(gstate),
                 var: var.sinto(gstate),
@@ -2916,7 +2912,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, ImplItem<Body>>
 {
     fn sinto(&self, s: &S) -> ImplItem<Body> {
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        let impl_item = tcx.hir().impl_item(self.id.clone());
+        let impl_item = tcx.hir().impl_item(self.id);
         let s = with_owner_id(s.base(), (), (), impl_item.owner_id.to_def_id());
         impl_item.sinto(&s)
     }
@@ -3024,7 +3020,7 @@ pub struct GenericParam<Body: IsBody> {
     pub pure_wrt_drop: bool,
     pub kind: GenericParamKind<Body>,
     pub colon_span: Option<Span>,
-    #[value(s.base().tcx.hir().attrs(hir_id.clone()).sinto(s))]
+    #[value(s.base().tcx.hir().attrs(*hir_id).sinto(s))]
     attributes: Vec<Attribute>,
 }
 
@@ -3195,7 +3191,7 @@ pub struct HirFieldDef {
     pub hir_id: HirId,
     pub def_id: GlobalIdent,
     pub ty: Ty,
-    #[value(s.base().tcx.hir().attrs(hir_id.clone()).sinto(s))]
+    #[value(s.base().tcx.hir().attrs(*hir_id).sinto(s))]
     attributes: Vec<Attribute>,
 }
 
@@ -3222,7 +3218,7 @@ pub struct Variant<Body: IsBody> {
     })]
     pub discr: DiscriminantDefinition,
     pub span: Span,
-    #[value(s.base().tcx.hir().attrs(hir_id.clone()).sinto(s))]
+    #[value(s.base().tcx.hir().attrs(*hir_id).sinto(s))]
     pub attributes: Vec<Attribute>,
 }
 
@@ -3236,7 +3232,7 @@ pub struct UsePath {
     #[map(x.iter().map(|res| res.sinto(s)).collect())]
     pub res: Vec<Res>,
     pub segments: Vec<PathSegment>,
-    #[value(self.segments.iter().last().map_or(None, |segment| {
+    #[value(self.segments.iter().last().and_then(|segment| {
             match s.base().tcx.hir_node_by_def_id(segment.hir_id.owner.def_id) {
                 rustc_hir::Node::Item(rustc_hir::Item {
                     ident,
@@ -3438,7 +3434,7 @@ impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto<S, TraitItem<Body>>
     fn sinto(&self, s: &S) -> TraitItem<Body> {
         let s = with_owner_id(s.base(), (), (), self.id.owner_id.to_def_id());
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        tcx.hir().trait_item(self.clone().id).sinto(&s)
+        tcx.hir().trait_item(self.id).sinto(&s)
     }
 }
 
@@ -3484,7 +3480,7 @@ impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto<S, ForeignItem<Body>>
 {
     fn sinto(&self, s: &S) -> ForeignItem<Body> {
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        tcx.hir().foreign_item(self.clone().id).sinto(s)
+        tcx.hir().foreign_item(self.id).sinto(s)
     }
 }
 
@@ -3543,7 +3539,7 @@ pub struct TraitRef {
 #[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
 pub struct TraitPredicate {
     pub trait_ref: TraitRef,
-    #[map(x.clone() == rustc_middle::ty::PredicatePolarity::Positive)]
+    #[map(*x == rustc_middle::ty::PredicatePolarity::Positive)]
     #[from(polarity)]
     pub is_positive: bool,
 }
@@ -3662,10 +3658,7 @@ pub struct Clause {
 impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause> for rustc_middle::ty::Clause<'tcx> {
     fn sinto(&self, s: &S) -> Clause {
         let kind = self.kind().sinto(s);
-        let id = kind
-            .clone()
-            .map(|clause_kind| PredicateKind::Clause(clause_kind))
-            .predicate_id();
+        let id = kind.clone().map(PredicateKind::Clause).predicate_id();
         Clause { kind, id }
     }
 }
@@ -3676,11 +3669,8 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause>
 {
     fn sinto(&self, s: &S) -> Clause {
         let kind: Binder<_> = self.sinto(s);
-        let kind: Binder<ClauseKind> = kind.map(|x| ClauseKind::Trait(x));
-        let id = kind
-            .clone()
-            .map(|clause_kind| PredicateKind::Clause(clause_kind))
-            .predicate_id();
+        let kind: Binder<ClauseKind> = kind.map(ClauseKind::Trait);
+        let id = kind.clone().map(PredicateKind::Clause).predicate_id();
         Clause { kind, id }
     }
 }
@@ -3993,7 +3983,7 @@ impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto<S, Item<Body>> for rustc_hir:
 impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto<S, Item<Body>> for rustc_hir::ItemId {
     fn sinto(&self, s: &S) -> Item<Body> {
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        tcx.hir().item(self.clone()).sinto(s)
+        tcx.hir().item(*self).sinto(s)
     }
 }
 
diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs
index ebcd38333..3a59a398f 100644
--- a/frontend/exporter/src/types/mir.rs
+++ b/frontend/exporter/src/types/mir.rs
@@ -76,7 +76,7 @@ fn name_of_local(
     var_debug_info: &Vec<rustc_middle::mir::VarDebugInfo>,
 ) -> Option<String> {
     var_debug_info
-        .into_iter()
+        .iter()
         .find(|info| {
             if let rustc_middle::mir::VarDebugInfoContents::Place(place) = info.value {
                 place.projection.is_empty() && place.local == local
@@ -803,7 +803,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
 
         loop {
             use rustc_middle::mir::ProjectionElem::*;
-            let cur_ty = current_ty.clone();
+            let cur_ty = current_ty;
             let cur_kind = current_kind.clone();
             use rustc_middle::ty::TyKind;
             let mk_field =
@@ -835,7 +835,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                 [Downcast(_, variant_idx), Field(index, ty), rest @ ..] => {
                     elems = rest;
                     let r = mk_field(index, Some(*variant_idx));
-                    current_ty = ty.clone();
+                    current_ty = *ty;
                     r
                 }
                 [elem, rest @ ..] => {
@@ -844,7 +844,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                     match elem {
                         Deref => {
                             current_ty = match current_ty.kind() {
-                                TyKind::Ref(_, ty, _) | TyKind::RawPtr(ty, _) => ty.clone(),
+                                TyKind::Ref(_, ty, _) | TyKind::RawPtr(ty, _) => *ty,
                                 TyKind::Adt(def, generics) if def.is_box() => generics.type_at(0),
                                 _ => supposely_unreachable_fatal!(
                                     s, "PlaceDerefNotRefNorPtrNorBox";
@@ -860,13 +860,13 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                                 use crate::rustc_index::Idx;
                                 let generics = generics.as_closure();
                                 let upvar_tys = generics.upvar_tys();
-                                current_ty = upvar_tys[index.sinto(s).index()].clone();
+                                current_ty = upvar_tys[index.sinto(s).index()];
                                 ProjectionElem::Field(ProjectionElemFieldKind::ClosureState(
                                     index.sinto(s),
                                 ))
                             } else {
                                 let r = mk_field(index, None);
-                                current_ty = ty.clone();
+                                current_ty = *ty;
                                 r
                             }
                         }
@@ -879,7 +879,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                                     {current_ty, current_kind, elem}
                                 );
                             };
-                            current_ty = ty.clone();
+                            current_ty = *ty;
                             ProjectionElem::Index(local.sinto(s))
                         }
                         ConstantIndex {
@@ -894,7 +894,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                                     {current_ty, current_kind, elem}
                                 )
                             };
-                            current_ty = ty.clone();
+                            current_ty = *ty;
                             ProjectionElem::ConstantIndex {
                                 offset: *offset,
                                 min_length: *min_length,
@@ -911,7 +911,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                             }
                         }
                         OpaqueCast(ty) => {
-                            current_ty = ty.clone();
+                            current_ty = *ty;
                             ProjectionElem::OpaqueCast
                         }
                         // This is used for casts to a subtype, e.g. between `for<‘a> fn(&’a ())`
diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs
index 0eaf64c9b..f18cf4eff 100644
--- a/frontend/exporter/src/types/new/full_def.rs
+++ b/frontend/exporter/src/types/new/full_def.rs
@@ -380,7 +380,7 @@ fn normalize_trait_clauses<'tcx, S: UnderOwnerState<'tcx>>(
     let predicates: Vec<_> = predicates
         .iter()
         .map(|(clause, span)| {
-            let mut clause = clause.clone();
+            let mut clause = *clause;
             if matches!(&clause.kind().skip_binder(), ty::ClauseKind::Trait(_)) {
                 clause = s
                     .base()
diff --git a/frontend/exporter/src/types/new/item_attributes.rs b/frontend/exporter/src/types/new/item_attributes.rs
index 673e8b04f..aeebd92c0 100644
--- a/frontend/exporter/src/types/new/item_attributes.rs
+++ b/frontend/exporter/src/types/new/item_attributes.rs
@@ -7,6 +7,12 @@ pub struct ItemAttributes {
     parent_attributes: Vec<Attribute>,
 }
 
+impl Default for ItemAttributes {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
 impl ItemAttributes {
     pub fn new() -> Self {
         ItemAttributes {
@@ -40,8 +46,7 @@ impl ItemAttributes {
             parent_attributes: hir
                 .parent_owner_iter(HirId::from(oid))
                 .map(|(oid, _)| oid)
-                .map(attrs_of)
-                .flatten()
+                .flat_map(attrs_of)
                 .collect(),
         }
     }
@@ -52,7 +57,7 @@ impl ItemAttributes {
         if let Some(def_id) = did.as_local() {
             Self::from_owner_id(s, rustc_hir::hir_id::OwnerId { def_id })
         } else {
-            return ItemAttributes::new();
+            ItemAttributes::new()
         }
     }
 }
diff --git a/frontend/exporter/src/types/serialize_int.rs b/frontend/exporter/src/types/serialize_int.rs
index 3d020ea3e..1b54020bf 100644
--- a/frontend/exporter/src/types/serialize_int.rs
+++ b/frontend/exporter/src/types/serialize_int.rs
@@ -34,7 +34,7 @@ pub mod unsigned {
         where
             E: serde::de::Error,
         {
-            Ok(v.parse().map_err(serde::de::Error::custom)?)
+            v.parse().map_err(serde::de::Error::custom)
         }
 
         fn visit_u64<E>(self, v: u64) -> Result<Self::Value, E>
@@ -75,7 +75,7 @@ pub mod signed {
         where
             E: serde::de::Error,
         {
-            Ok(v.parse().map_err(serde::de::Error::custom)?)
+            v.parse().map_err(serde::de::Error::custom)
         }
 
         fn visit_u64<E>(self, v: u64) -> Result<Self::Value, E>
diff --git a/frontend/exporter/src/utils.rs b/frontend/exporter/src/utils.rs
index fc5691f44..73843e7ce 100644
--- a/frontend/exporter/src/utils.rs
+++ b/frontend/exporter/src/utils.rs
@@ -150,9 +150,7 @@ mod s_expect_impls {
 
 macro_rules! s_assert {
     ($s:ident, $assertion:expr) => {{
-        if $assertion {
-            ()
-        } else {
+        if !($assertion) {
             fatal!($s, "assertion failed: {}", stringify!($assertion))
         }
     }};
diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index 22261bf84..a69da2fce 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -215,7 +215,7 @@ pub fn lemma(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
             return None;
         };
         let ps = (segments.len() == 1).then_some(()).and(segments.first())?;
-        (ps.ident.to_string() == "Proof").then_some(())?;
+        (ps.ident == "Proof").then_some(())?;
         let PathArguments::AngleBracketed(args) = &ps.arguments else {
             None?
         };
@@ -236,8 +236,7 @@ pub fn lemma(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
                     return ensures(
                         quote! {|_| #ensures_clause}.into(),
                         quote! { #attr #item }.into(),
-                    )
-                    .into();
+                    );
                 }
                 None => false,
             },
@@ -697,7 +696,7 @@ pub fn int(payload: pm::TokenStream) -> pm::TokenStream {
     let lit = format!("{lit}");
     // Allow negative numbers
     let mut lit = lit.strip_prefix("-").unwrap_or(lit.as_str()).to_string();
-    if let Some(faulty) = lit.chars().find(|ch| !matches!(ch, '0'..='9')) {
+    if let Some(faulty) = lit.chars().find(|ch| !ch.is_ascii_digit()) {
         abort_call_site!(format!("Expected a digit, found {faulty}"));
     }
     if negative {
diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs
index 6bd5282f1..d02bdea78 100644
--- a/hax-lib-macros/src/quote.rs
+++ b/hax-lib-macros/src/quote.rs
@@ -27,15 +27,12 @@ enum AntiquoteKind {
 
 impl ToTokens for AntiquoteKind {
     fn to_tokens(&self, tokens: &mut TokenStream) {
-        tokens.extend(
-            [match self {
-                Self::Expr => quote! {_expr},
-                Self::Constructor => quote! {_constructor},
-                Self::Pat => quote! {_pat},
-                Self::Ty => quote! {_ty},
-            }]
-            .into_iter(),
-        )
+        tokens.extend([match self {
+            Self::Expr => quote! {_expr},
+            Self::Constructor => quote! {_constructor},
+            Self::Pat => quote! {_pat},
+            Self::Ty => quote! {_ty},
+        }])
     }
 }
 
@@ -59,7 +56,7 @@ impl ToTokens for Antiquote {
             AntiquoteKind::Pat => wrap_pattern(ts),
             AntiquoteKind::Ty => quote! {None::<#ts>},
         };
-        tokens.extend([ts].into_iter())
+        tokens.extend([ts])
     }
 }
 
@@ -85,7 +82,7 @@ fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), Stri
                 if let Some('{') = chars.peek() {
                     chars.next(); // Consume `{`
                     let mut level = 0;
-                    while let Some(ch) = chars.next() {
+                    for ch in chars.by_ref() {
                         level += match ch {
                             '{' => 1,
                             '}' => -1,
@@ -180,7 +177,7 @@ pub(super) fn detect_future_node_in_expression(e: &syn::Expr) -> bool {
 pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::TokenStream {
     let (mut backend_code, antiquotes) = {
         let payload = parse_macro_input!(payload as LitStr).value();
-        if payload.find(SPLIT_MARK).is_some() {
+        if payload.contains(SPLIT_MARK) {
             return quote! {std::compile_error!(std::concat!($SPLIT_MARK, " is reserved"))}.into();
         }
         let (string, antiquotes) = match process_string(&payload) {
diff --git a/hax-lib-macros/src/rewrite_self.rs b/hax-lib-macros/src/rewrite_self.rs
index 364f4d88a..6a92040cc 100644
--- a/hax-lib-macros/src/rewrite_self.rs
+++ b/hax-lib-macros/src/rewrite_self.rs
@@ -107,16 +107,15 @@ impl visit_mut::VisitMut for RewriteSelf {
                     attrs: vec![],
                     by_ref: None,
                     mutability: None,
-                    ident: self.self_ident(span.clone()).clone(),
+                    ident: self.self_ident(span).clone(),
                     subpat: None,
                 })),
                 colon_token: token::Colon(arg.span()),
-                ty: Box::new(self.self_ty(span.clone())),
+                ty: Box::new(self.self_ty(span)),
             });
         }
     }
     fn visit_item_impl_mut(&mut self, _i: &mut ItemImpl) {
         // Do nothing! We allow user to write self if it's nested in a impl block
-        ()
     }
 }
diff --git a/hax-lib-macros/src/syn_ext.rs b/hax-lib-macros/src/syn_ext.rs
index 83e8dd746..316ab84f1 100644
--- a/hax-lib-macros/src/syn_ext.rs
+++ b/hax-lib-macros/src/syn_ext.rs
@@ -52,7 +52,7 @@ impl PathExt for Path {
                 return None;
             }
         }
-        return Some(chunks);
+        Some(chunks)
     }
 }
 
@@ -70,7 +70,7 @@ pub trait ExpectIdent {
 
 impl<T: ExpectIdent> ExpectIdent for Box<T> {
     fn expect_ident(&self) -> Option<Ident> {
-        let this: &T = &*self;
+        let this: &T = self;
         this.expect_ident()
     }
 }
diff --git a/hax-lib-macros/src/utils.rs b/hax-lib-macros/src/utils.rs
index b155855e8..c1c974a39 100644
--- a/hax-lib-macros/src/utils.rs
+++ b/hax-lib-macros/src/utils.rs
@@ -80,11 +80,7 @@ pub(crate) fn merge_generics(x: Generics, y: Generics) -> Generics {
         where_clause: match (x.where_clause, y.where_clause) {
             (Some(wx), Some(wy)) => Some(syn::WhereClause {
                 where_token: wx.where_token,
-                predicates: wx
-                    .predicates
-                    .into_iter()
-                    .chain(wy.predicates.into_iter())
-                    .collect(),
+                predicates: wx.predicates.into_iter().chain(wy.predicates).collect(),
             }),
             (Some(w), None) | (None, Some(w)) => Some(w),
             (None, None) => None,
@@ -182,7 +178,7 @@ impl VisitMut for RewriteFuture {
                     }
                 };
                 let help_message = match self.0.iter().next() {
-                    None => format!(" In the context, there is no `&mut` input."),
+                    None => " In the context, there is no `&mut` input.".to_string(),
                     Some(var) => {
                         format!(" For example, in the context you can write `future({var})`.")
                     }
diff --git a/hax-lib-protocol-macros/src/lib.rs b/hax-lib-protocol-macros/src/lib.rs
index db9945abe..75d39ad12 100644
--- a/hax-lib-protocol-macros/src/lib.rs
+++ b/hax-lib-protocol-macros/src/lib.rs
@@ -76,7 +76,7 @@ pub fn init(
     );
     output.extend(expanded);
 
-    return output.into();
+    output.into()
 }
 
 /// This macro takes an `fn` as the basis of an `InitialState` implementation
@@ -236,7 +236,7 @@ pub fn write(
     );
     output.extend(expanded);
 
-    return output.into();
+    output.into()
 }
 
 /// Macro deriving a `ReadState` implementation for the destination state type,
@@ -305,5 +305,5 @@ pub fn read(
     );
     output.extend(expanded);
 
-    return output.into();
+    output.into()
 }