diff --git a/CHANGELOG.md b/CHANGELOG.md
index 512788b24..05aedee00 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,6 +33,7 @@ Changes to the Lean backend:
  - Add support for default methods of traits (#1777)
  - Add support for pattern matching on constant literals (#1789)
  - Add support for binding subpatterns in match constructs (#1790)
+ - Add error when using patterns in function parameters (#1792)
 
 Miscellaneous:
 - Reserve extraction folder for auto-generated files in Lean examples (#1754)
diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs
index e153eb36a..0147bb7cd 100644
--- a/rust-engine/src/backends/lean.rs
+++ b/rust-engine/src/backends/lean.rs
@@ -850,7 +850,14 @@ set_option linter.unusedVariables false
         }
 
         fn param(&self, param: &Param) -> DocBuilder<A> {
-            self.pat_typed(&param.pat)
+            if matches!(
+                *param.pat.kind,
+                PatKind::Wild | PatKind::Ascription { .. } | PatKind::Binding { sub_pat: None, .. }
+            ) {
+                self.pat_typed(&param.pat)
+            } else {
+                emit_error!(issue 1791, "Function parameters must not contain patterns")
+            }
         }
 
         fn item(&self, Item { ident, kind, meta }: &Item) -> DocBuilder<A> {