add test

leanprover · May 2, 2024 · 61a9c45 · 61a9c45
1 parent 46bbaab
commit 61a9c45
Showing 1 changed file with 5 additions and 0 deletions.
diff --git 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