diff --git a/tests/lean/structDefault.lean b/tests/lean/structDefault.lean
new file mode 100644
index 0000000000..40d549ef34
--- /dev/null
+++ b/tests/lean/structDefault.lean
@@ -0,0 +1,11 @@
+structure A where
+  f : Nat → Nat → Nat
+
+structure B extends A where
+  f (a b : Nat) := 10
+
+structure C extends A where
+  f a b := 0
+
+structure D extends A where
+  f a b := true -- error
diff --git a/tests/lean/structDefault.lean.expected.out b/tests/lean/structDefault.lean.expected.out
new file mode 100644
index 0000000000..ac18a5414b
--- /dev/null
+++ b/tests/lean/structDefault.lean.expected.out
@@ -0,0 +1,6 @@
+structDefault.lean:11:11: error: type mismatch
+  true
+has type
+  Bool
+but is expected to have type
+  Nat