From ef87b33cdc26e707dcfb1cc9cf6dbc7dbd4212a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Sep 2020 17:18:20 -0700
Subject: [PATCH] test: add another missing hole test

---
 tests/lean/holes.lean              | 4 ++++
 tests/lean/holes.lean.expected.out | 5 +++++
 2 files changed, 9 insertions(+)

diff --git a/tests/lean/holes.lean b/tests/lean/holes.lean
index 5fe9a4e6be..ac72e420ad 100644
--- a/tests/lean/holes.lean
+++ b/tests/lean/holes.lean
@@ -20,3 +20,7 @@ f a
 
 partial def f7 (x : Nat) :=
 f7 x
+
+partial def f8 (x : Nat) :=
+let rec aux (y : Nat) := aux y;
+x + 1
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index 9b0cc34dfa..5239c0f0c0 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -49,3 +49,8 @@ holes.lean:21:25: error: don't know how to synthesize placeholder
 context:
 x : Nat
 ⊢ Sort ?
+holes.lean:25:8: error: don't know how to synthesize placeholder
+context:
+f8 : Nat → Nat
+x y : Nat
+⊢ Sort ?