add test

leanprover · May 2, 2024 · 2f58949 · 2f58949
1 parent 61a9c45
commit 2f58949
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/tests/lean/run/autoparam.lean b/tests/lean/run/autoparam.lean
@@ -8,4 +8,8 @@ f x y
 def f2 (x y : Nat) (h : x = y := by exact rfl) : Nat :=
 x + x
 
+def f3 (x y : Nat) (h : x = y := by exact Eq.refl x) : Nat :=
+x + x
+
 #check fun x => f2 x x
+#check fun x => f3 x x