diff --git a/crates/formality-check/src/coherence.rs b/crates/formality-check/src/coherence.rs
index d5c4cda7..9d57d29b 100644
--- a/crates/formality-check/src/coherence.rs
+++ b/crates/formality-check/src/coherence.rs
@@ -140,7 +140,7 @@ impl Check<'_> {
                     &a.where_clauses,
                     &b.where_clauses,
                 ),
-                &inverted_wc,
+                inverted_wc,
             )
             .is_ok()
         }) {
diff --git a/crates/formality-macros/src/cast.rs b/crates/formality-macros/src/cast.rs
index f9ddf854..9a69d38e 100644
--- a/crates/formality-macros/src/cast.rs
+++ b/crates/formality-macros/src/cast.rs
@@ -7,7 +7,7 @@ pub(crate) fn upcast_impls(s: synstructure::Structure) -> Vec<TokenStream> {
     let num_variants = s.variants().len();
     s.variants()
         .iter()
-        .filter(|v| num_variants == 1 || has_cast_attr(&v.ast().attrs))
+        .filter(|v| num_variants == 1 || has_cast_attr(v.ast().attrs))
         .map(|v| upcast_to_variant(&s, v))
         .chain(Some(self_upcast(&s)))
         .collect()
@@ -46,7 +46,7 @@ pub(crate) fn downcast_impls(s: synstructure::Structure) -> Vec<TokenStream> {
     let num_variants = s.variants().len();
     s.variants()
         .iter()
-        .filter(|v| num_variants == 1 || has_cast_attr(&v.ast().attrs))
+        .filter(|v| num_variants == 1 || has_cast_attr(v.ast().attrs))
         .map(|v| downcast_to_variant(&s, v))
         .chain(Some(self_downcast(&s)))
         .collect()
@@ -91,5 +91,5 @@ fn downcast_to_variant(s: &synstructure::Structure, v: &VariantInfo) -> TokenStr
 }
 
 pub(crate) fn has_cast_attr(attrs: &[Attribute]) -> bool {
-    attrs.iter().find(|a| a.path.is_ident("cast")).is_some()
+    attrs.iter().any(|a| a.path.is_ident("cast"))
 }
diff --git a/crates/formality-macros/src/debug.rs b/crates/formality-macros/src/debug.rs
index 00851a82..e29fa0f0 100644
--- a/crates/formality-macros/src/debug.rs
+++ b/crates/formality-macros/src/debug.rs
@@ -43,7 +43,7 @@ fn debug_variant(
 
     // When invoked like `#[term(foo)]`, use the spec from `foo`
     if let Some(spec) = external_spec {
-        return debug_variant_with_attr(variant, &spec);
+        return debug_variant_with_attr(variant, spec);
     }
 
     // Else, look for a `#[grammar]` attribute on the variant
@@ -58,7 +58,7 @@ fn debug_variant(
 
     if variant.bindings().is_empty() {
         // No bindings (e.g., `Foo`) -- just parse a keyword `foo`
-        let literal = Literal::string(&to_parse_ident(&ast.ident));
+        let literal = Literal::string(&to_parse_ident(ast.ident));
         quote! {
             write!(fmt, #literal)?;
         }
@@ -79,7 +79,7 @@ fn debug_variant(
         quote!(#(#streams)*)
     } else {
         // Otherwise -- parse `variant(binding0, ..., bindingN)`
-        let literal = Literal::string(&to_parse_ident(&ast.ident));
+        let literal = Literal::string(&to_parse_ident(ast.ident));
         let binding_names: Vec<_> = variant.bindings().iter().map(|b| &b.binding).collect();
         quote! {
             fmt.debug_tuple(#literal)
diff --git a/crates/formality-macros/src/fixed_point.rs b/crates/formality-macros/src/fixed_point.rs
index 570be111..71a84762 100644
--- a/crates/formality-macros/src/fixed_point.rs
+++ b/crates/formality-macros/src/fixed_point.rs
@@ -35,7 +35,7 @@ impl syn::parse::Parse for FixedPointArgs {
         while !input.is_empty() {
             let ident: syn::Ident = input.parse()?;
             let _: syn::Token!(=) = input.parse()?;
-            if ident.to_string() == "default" {
+            if ident == "default" {
                 let expr: syn::Expr = input.parse()?;
                 args.default = Some(expr);
             } else {
@@ -226,7 +226,7 @@ fn validate_arg_pattern(pat: &syn::Pat) -> syn::Result<(syn::Ident, Option<syn::
                 ));
             }
 
-            Ok((ident.ident.clone(), ident.mutability.clone()))
+            Ok((ident.ident.clone(), ident.mutability))
         }
         _ => Err(syn::Error::new_spanned(
             pat,
@@ -245,7 +245,7 @@ fn validate_arg_ty(ty: &syn::Type) -> syn::Result<(bool, syn::Type)> {
                 ));
             }
 
-            if let Some(_) = &r.lifetime {
+            if r.lifetime.is_some() {
                 return Err(syn::Error::new_spanned(
                     ty,
                     "named lifetimes not permitted in fixed-point functions",
@@ -265,19 +265,15 @@ fn validate_arg_ty(ty: &syn::Type) -> syn::Result<(bool, syn::Type)> {
 
 fn validate_ty(ty: &syn::Type) -> syn::Result<()> {
     match ty {
-        syn::Type::ImplTrait(_) => {
-            return Err(syn::Error::new_spanned(
-                ty,
-                "impl Trait types not allowed in fixed-point functions",
-            ));
-        }
+        syn::Type::ImplTrait(_) => Err(syn::Error::new_spanned(
+            ty,
+            "impl Trait types not allowed in fixed-point functions",
+        )),
 
-        syn::Type::Reference(_) => {
-            return Err(syn::Error::new_spanned(
-                ty,
-                "reference types only allowed at the top-level in fixed-point functions",
-            ));
-        }
+        syn::Type::Reference(_) => Err(syn::Error::new_spanned(
+            ty,
+            "reference types only allowed at the top-level in fixed-point functions",
+        )),
 
         _ => Ok(()),
     }
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index 7e9eb323..668862a9 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -31,7 +31,7 @@ pub(crate) fn derive_parse_with_spec(
             let mut __results = vec![];
         });
         for variant in s.variants() {
-            let variant_name = as_literal(&variant.ast().ident);
+            let variant_name = as_literal(variant.ast().ident);
             let v = parse_variant(variant, None)?;
             stream.extend(quote! {
                 __results.push({
@@ -69,7 +69,7 @@ fn parse_variant(
 
     // When invoked like `#[term(foo)]`, use the spec from `foo`
     if let Some(spec) = external_spec {
-        return parse_variant_with_attr(variant, &spec);
+        return parse_variant_with_attr(variant, spec);
     }
 
     // Else, look for a `#[grammar]` attribute on the variant
@@ -81,7 +81,7 @@ fn parse_variant(
 
     if variant.bindings().is_empty() {
         // No bindings (e.g., `Foo`) -- just parse a keyword `foo`
-        let literal = Literal::string(&to_parse_ident(&ast.ident));
+        let literal = Literal::string(&to_parse_ident(ast.ident));
         let construct = variant.construct(|_, _| quote! {});
         Ok(quote! {
             let ((), text) = parse::expect_keyword(#literal, text)?;
@@ -97,7 +97,7 @@ fn parse_variant(
         })
     } else {
         // Otherwise -- parse `variant(binding0, ..., bindingN)`
-        let literal = Literal::string(&to_parse_ident(&ast.ident));
+        let literal = Literal::string(&to_parse_ident(ast.ident));
         let build: Vec<TokenStream> = parse_bindings(variant.bindings());
         let construct = variant.construct(field_ident);
         Ok(quote! {
@@ -199,7 +199,7 @@ fn lookahead(for_field: &Ident, op: Option<&FormalitySpecOp>) -> syn::Result<Lit
         Some(FormalitySpecOp::Keyword { .. }) | Some(FormalitySpecOp::Field { .. }) | None => {
             Err(syn::Error::new_spanned(
                 for_field,
-                format!("cannot use `*` or `,` without lookahead"),
+                "cannot use `*` or `,` without lookahead".to_string(),
             ))
         }
     }
diff --git a/crates/formality-macros/src/spec.rs b/crates/formality-macros/src/spec.rs
index 2cbe6a92..9faad894 100644
--- a/crates/formality-macros/src/spec.rs
+++ b/crates/formality-macros/src/spec.rs
@@ -129,5 +129,5 @@ fn parse_variable_binding(
         _ => return error(),
     };
 
-    Ok(FormalitySpecOp::Field { name, mode: mode })
+    Ok(FormalitySpecOp::Field { name, mode })
 }
diff --git a/crates/formality-prove/src/prove/combinators.rs b/crates/formality-prove/src/prove/combinators.rs
index 169137f7..54583e46 100644
--- a/crates/formality-prove/src/prove/combinators.rs
+++ b/crates/formality-prove/src/prove/combinators.rs
@@ -31,7 +31,7 @@ where
             let context = c1.substitution().apply(context);
             let a = c1.substitution().apply(&a);
             let b = c1.substitution().apply(&b);
-            zip(&decls, c1.env(), &context, a, b, op)
+            zip(decls, c1.env(), &context, a, b, op)
                 .into_iter()
                 .map(move |c2| c1.seq(c2))
         })
@@ -60,7 +60,7 @@ where
         .flat_map(|c1| {
             let context = c1.substitution().apply(context);
             let a_remaining = c1.substitution().apply(&a_remaining);
-            for_all(&decls, c1.env(), &context, &a_remaining, op)
+            for_all(decls, c1.env(), &context, &a_remaining, op)
                 .into_iter()
                 .map(move |c2| c1.seq(c2))
         })
diff --git a/crates/formality-prove/src/prove/env.rs b/crates/formality-prove/src/prove/env.rs
index 19a0f165..ff3a7f4e 100644
--- a/crates/formality-prove/src/prove/env.rs
+++ b/crates/formality-prove/src/prove/env.rs
@@ -186,8 +186,8 @@ impl Env {
 
         let p0 = v[0];
         let universe_p0 = self.universe(p0);
-        for i in 1..v.len() {
-            assert_eq!(self.universe(v[i]).index, universe_p0.index + i);
+        for (i, item) in v.iter().enumerate().skip(1) {
+            assert_eq!(self.universe(item).index, universe_p0.index + i);
         }
 
         self.variables.drain(universe_p0.index..).collect()
diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs
index e7b32175..6e86521d 100644
--- a/crates/formality-prove/src/prove/prove_wc.rs
+++ b/crates/formality-prove/src/prove/prove_wc.rs
@@ -54,8 +54,8 @@ judgment_fn! {
             (let i = i.binder.instantiate_with(&subst).unwrap())
             (let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap())
             (let co_assumptions = (&assumptions, &trait_ref))
-            (prove(&decls, env, &co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
-            (prove_after(&decls, c, &co_assumptions, &i.where_clause) => c)
+            (prove(&decls, env, co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
+            (prove_after(&decls, c, co_assumptions, &i.where_clause) => c)
             (prove_after(&decls, c, &assumptions, &t.where_clause) => c)
             ----------------------------- ("positive impl")
             (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs
index 37cef86b..f9698bb0 100644
--- a/crates/formality-rust/src/grammar.rs
+++ b/crates/formality-rust/src/grammar.rs
@@ -34,7 +34,7 @@ impl Program {
                 _ => None,
             })
             .collect();
-        if traits.len() < 1 {
+        if traits.is_empty() {
             anyhow::bail!("no trait named `{trait_id:?}`")
         } else if traits.len() > 1 {
             anyhow::bail!("multiple traits named `{trait_id:?}`")
@@ -84,9 +84,9 @@ impl Struct {
         Adt {
             id: self.id.clone(),
             binder: Binder::new(
-                &vars,
+                vars,
                 AdtBoundData {
-                    where_clauses: where_clauses,
+                    where_clauses,
                     variants: vec![Variant {
                         name: VariantId::for_struct(),
                         fields,
diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs
index b3e1dc5b..4325dd1d 100644
--- a/crates/formality-rust/src/prove.rs
+++ b/crates/formality-rust/src/prove.rs
@@ -91,7 +91,7 @@ impl Crate {
                     Some(prove::TraitDecl {
                         id: id.clone(),
                         binder: Binder::new(
-                            &vars,
+                            vars,
                             prove::TraitDeclBoundData {
                                 where_clause: where_clauses
                                     .iter()
@@ -123,7 +123,7 @@ impl Crate {
                     ) = binder.open();
                     Some(prove::ImplDecl {
                         binder: Binder::new(
-                            &vars,
+                            vars,
                             prove::ImplDeclBoundData {
                                 trait_ref: trait_id.with(self_ty, trait_parameters),
                                 where_clause: where_clauses.to_wcs(),
@@ -152,7 +152,7 @@ impl Crate {
                     ) = binder.open();
                     Some(prove::NegImplDecl {
                         binder: Binder::new(
-                            &vars,
+                            vars,
                             prove::NegImplDeclBoundData {
                                 trait_ref: trait_id.with(self_ty, trait_parameters),
                                 where_clause: where_clauses.to_wcs(),
@@ -259,8 +259,7 @@ impl Crate {
                                 .iter()
                                 .map(|e| {
                                     let fresh_var = fresh_bound_var(ParameterKind::Ty);
-                                    let ensures =
-                                        Binder::new(&vec![fresh_var], e.to_wc(&fresh_var));
+                                    let ensures = Binder::new(vec![fresh_var], e.to_wc(fresh_var));
 
                                     prove::AliasBoundDecl {
                                         binder: Binder::new(
diff --git a/crates/formality-rust/src/trait_binder.rs b/crates/formality-rust/src/trait_binder.rs
index 8a2d0955..9d901ad8 100644
--- a/crates/formality-rust/src/trait_binder.rs
+++ b/crates/formality-rust/src/trait_binder.rs
@@ -105,7 +105,7 @@ where
         let (data, text) = T::parse(&scope1, text)?;
 
         let bound_vars: Vec<BoundVar> = bindings.iter().map(|b| b.bound_var).collect();
-        let explicit_binder = Binder::new(&bound_vars, data);
+        let explicit_binder = Binder::new(bound_vars, data);
 
         Ok((TraitBinder { explicit_binder }, text))
     }
diff --git a/crates/formality-types/src/cast.rs b/crates/formality-types/src/cast.rs
index 77d425f2..7041633b 100644
--- a/crates/formality-types/src/cast.rs
+++ b/crates/formality-types/src/cast.rs
@@ -203,7 +203,7 @@ where
     T: Upcast<U>,
 {
     fn upcast_from(term: &[T]) -> Self {
-        term.into_iter().map(|t| t.upcast()).collect()
+        term.iter().map(|t| t.upcast()).collect()
     }
 }
 
diff --git a/crates/formality-types/src/collections.rs b/crates/formality-types/src/collections.rs
index bf61b5a7..8f33a485 100644
--- a/crates/formality-types/src/collections.rs
+++ b/crates/formality-types/src/collections.rs
@@ -69,11 +69,7 @@ pub trait SetExt<T>: Sized {
 impl<T: Ord + Clone> SetExt<T> for Set<T> {
     fn split_first(self) -> Option<(T, Set<T>)> {
         let mut iter = self.into_iter();
-        if let Some(e) = iter.next() {
-            Some((e, iter.collect()))
-        } else {
-            None
-        }
+        iter.next().map(|e| (e, iter.collect()))
     }
 
     fn union_with(mut self, other: Self) -> Self {
diff --git a/crates/formality-types/src/fixed_point/stack.rs b/crates/formality-types/src/fixed_point/stack.rs
index f094f8ec..906ebf8e 100644
--- a/crates/formality-types/src/fixed_point/stack.rs
+++ b/crates/formality-types/src/fixed_point/stack.rs
@@ -77,7 +77,7 @@ where
         }
 
         top.output = output;
-        return top.has_dependents;
+        top.has_dependents
     }
 
     /// Pops the top entry from the stack, returning the saved outputs.
diff --git a/crates/formality-types/src/fold.rs b/crates/formality-types/src/fold.rs
index 0d393465..07858872 100644
--- a/crates/formality-types/src/fold.rs
+++ b/crates/formality-types/src/fold.rs
@@ -80,7 +80,7 @@ impl Fold for Const {
                 v.substitute(substitution_fn),
                 ty.substitute(substitution_fn),
             ),
-            ConstData::Variable(v) => match substitution_fn(v.clone()) {
+            ConstData::Variable(v) => match substitution_fn(*v) {
                 None => self.clone(),
                 Some(Parameter::Const(c)) => c,
                 Some(param) => panic!("ill-kinded substitute: expected const, got {param:?}"),
@@ -121,9 +121,7 @@ impl Fold for u32 {
 }
 
 impl Fold for () {
-    fn substitute(&self, _substitution_fn: SubstitutionFn<'_>) -> Self {
-        ()
-    }
+    fn substitute(&self, _substitution_fn: SubstitutionFn<'_>) -> Self {}
 }
 
 impl<A: Fold, B: Fold> Fold for (A, B) {
diff --git a/crates/formality-types/src/grammar/binder.rs b/crates/formality-types/src/grammar/binder.rs
index 7ec16c14..60bc8d53 100644
--- a/crates/formality-types/src/grammar/binder.rs
+++ b/crates/formality-types/src/grammar/binder.rs
@@ -49,7 +49,7 @@ impl<T: Fold> Binder<T> {
 
     pub fn dummy(term: T) -> Self {
         let v: Vec<Variable> = vec![];
-        Self::new(&v, term)
+        Self::new(v, term)
     }
 
     /// Given a set of variables (X, Y, Z) and a term referecing some subset of them,
@@ -81,9 +81,9 @@ impl<T: Fold> Binder<T> {
     pub fn mentioned(variables: impl Upcast<Vec<Variable>>, term: T) -> Self {
         let mut variables: Vec<Variable> = variables.upcast();
         let fv = term.free_variables();
-        variables.retain(|v| fv.contains(&v));
+        variables.retain(|v| fv.contains(v));
         let variables: Vec<Variable> = variables.into_iter().collect();
-        Binder::new(&variables, term)
+        Binder::new(variables, term)
     }
 
     pub fn into<U>(self) -> Binder<U>
@@ -101,6 +101,10 @@ impl<T: Fold> Binder<T> {
         self.kinds.len()
     }
 
+    pub fn is_empty(&self) -> bool {
+        self.kinds.is_empty()
+    }
+
     /// Instantiate the binder with the given parameters, returning an err if the parameters
     /// are the wrong number or ill-kinded.
     pub fn instantiate_with(&self, parameters: &[impl Upcast<Parameter>]) -> Fallible<T> {
@@ -136,7 +140,7 @@ impl<T: Fold> Binder<T> {
                 debruijn: Some(DebruijnIndex::INNERMOST),
                 var_index,
                 kind: _,
-            }) => Some(substitution[var_index.index as usize].clone()),
+            }) => Some(substitution[var_index.index].clone()),
 
             _ => None,
         })
@@ -156,7 +160,7 @@ impl<T: Fold> Binder<T> {
     pub fn map<U: Fold>(&self, op: impl FnOnce(T) -> U) -> Binder<U> {
         let (vars, t) = self.open();
         let u = op(t);
-        Binder::new(&vars, u)
+        Binder::new(vars, u)
     }
 }
 
diff --git a/crates/formality-types/src/grammar/consts.rs b/crates/formality-types/src/grammar/consts.rs
index e032cc1a..3cfa87b9 100644
--- a/crates/formality-types/src/grammar/consts.rs
+++ b/crates/formality-types/src/grammar/consts.rs
@@ -29,7 +29,7 @@ impl Const {
     pub fn as_variable(&self) -> Option<Variable> {
         match self.data() {
             ConstData::Value(_, _) => None,
-            ConstData::Variable(var) => Some(var.clone()),
+            ConstData::Variable(var) => Some(*var),
         }
     }
 
diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs
index 2d842b38..0446e8cf 100644
--- a/crates/formality-types/src/grammar/ty.rs
+++ b/crates/formality-types/src/grammar/ty.rs
@@ -336,7 +336,7 @@ impl Lt {
 
     pub fn as_variable(&self) -> Option<Variable> {
         match self.data() {
-            LtData::Variable(v) => Some(v.clone()),
+            LtData::Variable(v) => Some(*v),
             _ => None,
         }
     }
@@ -381,7 +381,7 @@ impl Visit for LtData {
         match self {
             LtData::Variable(v) => {
                 if v.is_free() {
-                    vec![v.clone()]
+                    vec![*v]
                 } else {
                     vec![]
                 }
@@ -439,7 +439,7 @@ impl Variable {
             }
             .upcast()
         } else {
-            self.clone()
+            *self
         }
     }
 
@@ -462,7 +462,7 @@ impl Variable {
                 .upcast()
             })
         } else {
-            Some(self.clone())
+            Some(*self)
         }
     }
 
diff --git a/crates/formality-types/src/judgment.rs b/crates/formality-types/src/judgment.rs
index 492bd58b..e206ac45 100644
--- a/crates/formality-types/src/judgment.rs
+++ b/crates/formality-types/src/judgment.rs
@@ -7,9 +7,11 @@ mod test_reachable;
 
 pub type JudgmentStack<J, O> = RefCell<FixedPointStack<J, BTreeSet<O>>>;
 
+type InferenceRuleClosure<I, O> = Arc<dyn Fn(&I) -> Vec<O> + Send>;
+
 #[derive(Clone)]
 struct InferenceRule<I, O> {
-    closure: Arc<dyn Fn(&I) -> Vec<O> + Send>,
+    closure: InferenceRuleClosure<I, O>,
 }
 
 #[macro_export]
diff --git a/crates/formality-types/src/parse.rs b/crates/formality-types/src/parse.rs
index b5618644..cbb9d8a2 100644
--- a/crates/formality-types/src/parse.rs
+++ b/crates/formality-types/src/parse.rs
@@ -252,7 +252,7 @@ where
         let (data, text) = T::parse(&scope1, text)?;
 
         let kvis: Vec<BoundVar> = bindings.iter().map(|b| b.bound_var).collect();
-        Ok((Binder::new(&kvis, data), text))
+        Ok((Binder::new(kvis, data), text))
     }
 }
 
@@ -326,8 +326,8 @@ pub fn expect_char(ch: char, text0: &str) -> ParseResult<'_, ()> {
 /// Consume a comma if one is present.
 #[tracing::instrument(level = "trace", ret)]
 pub fn skip_trailing_comma(text: &str) -> &str {
-    if text.starts_with(",") {
-        &text[1..]
+    if let Some(stripped) = text.strip_prefix(',') {
+        stripped
     } else {
         text
     }
@@ -339,14 +339,8 @@ pub fn skip_trailing_comma(text: &str) -> &str {
 pub fn identifier(text: &str) -> ParseResult<'_, String> {
     accumulate(
         text,
-        |ch| match ch {
-            'a'..='z' | 'A'..='Z' | '_' => true,
-            _ => false,
-        },
-        |ch| match ch {
-            'a'..='z' | 'A'..='Z' | '_' | '0'..='9' => true,
-            _ => false,
-        },
+        |ch| matches!(ch, 'a'..='z' | 'A'..='Z' | '_'),
+        |ch| matches!(ch, 'a'..='z' | 'A'..='Z' | '_' | '0'..='9'),
         "identifier",
     )
 }
diff --git a/src/lib.rs b/src/lib.rs
index 72f9d8cf..ccb9029a 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -40,12 +40,12 @@ pub fn main() -> anyhow::Result<()> {
 }
 
 pub fn test_program_ok(input: &str) -> anyhow::Result<()> {
-    let program: Program = try_term(&input)?;
+    let program: Program = try_term(input)?;
     check_all_crates(&program)
 }
 
 pub fn test_where_clause(program: &str, assertion: &str) -> anyhow::Result<Set<Constraints>> {
-    let program: Program = try_term(&program)?;
+    let program: Program = try_term(program)?;
     check_all_crates(&program)?;
     let assertion: Arc<TestAssertion> = try_term(assertion)?;
     let decls = program.to_prove_decls();
diff --git a/src/main.rs b/src/main.rs
index b369dfda..6e883a15 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,3 +1,3 @@
 fn main() -> anyhow::Result<()> {
-    formality_core::with_tracing_logs(|| formality::main())
+    formality_core::with_tracing_logs(formality::main)
 }