diff --git a/tests/lean/run/autoparam.lean b/tests/lean/run/autoparam.lean index 294708797e07..377b4f9ee892 100644 --- a/tests/lean/run/autoparam.lean +++ b/tests/lean/run/autoparam.lean @@ -4,3 +4,8 @@ x + x def g (x y z : Nat) (h : x = y) : Nat := f x y + +def f2 (x y : Nat) (h : x = y := by exact rfl) : Nat := +x + x + +#check fun x => f2 x x