From 628633d02e7274429c247dcef7d093b72931860c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 17 Jan 2024 12:17:34 +0100
Subject: [PATCH] test: failed to infer implicit target (#3189)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The `induction` tactic complains if implicit targets cannot be inferred,
let’s test that.
---
 tests/lean/indimpltarget.lean              | 30 ++++++++++++++++++++++
 tests/lean/indimpltarget.lean.expected.out |  5 ++++
 2 files changed, 35 insertions(+)
 create mode 100644 tests/lean/indimpltarget.lean
 create mode 100644 tests/lean/indimpltarget.lean.expected.out

diff --git a/tests/lean/indimpltarget.lean b/tests/lean/indimpltarget.lean
new file mode 100644
index 0000000000..3008fd14a1
--- /dev/null
+++ b/tests/lean/indimpltarget.lean
@@ -0,0 +1,30 @@
+namespace Ex1
+
+theorem elim_with_implicit_target (motive : Nat → Nat → Prop) (case1  : ∀ m n, motive m n) (n : Nat) {m : Nat} : motive m n := case1 _ _
+
+example (n m : Nat) : n ≤ m := by
+  induction n using elim_with_implicit_target
+  case case1 => sorry
+
+end Ex1
+
+namespace Ex2
+
+theorem elim_with_implicit_target (motive : Nat → Nat → Prop) (case1  : ∀ m n, motive m n) {n : Nat} (m : Nat) : motive m n := case1 _ _
+
+example (n m : Nat) : n ≤ m := by
+  induction m using elim_with_implicit_target
+  case case1 => sorry
+
+end Ex2
+
+namespace Ex3
+
+-- this one should work
+theorem elim_with_implicit_target (motive : (n : Nat) → Fin n → Prop) (case1  : ∀ m n, motive m n) {n : Nat} (m : Fin n) : motive n m := case1 _ _
+
+example (n : Nat) (m : Fin n) : n ≤ m := by
+  induction m using elim_with_implicit_target
+  case case1 => sorry
+
+end Ex3
diff --git a/tests/lean/indimpltarget.lean.expected.out b/tests/lean/indimpltarget.lean.expected.out
new file mode 100644
index 0000000000..797357e144
--- /dev/null
+++ b/tests/lean/indimpltarget.lean.expected.out
@@ -0,0 +1,5 @@
+indimpltarget.lean:6:2-6:45: error: failed to infer implicit target, it contains unresolved metavariables
+  ?m
+indimpltarget.lean:16:2-16:45: error: failed to infer implicit target, it contains unresolved metavariables
+  ?m
+indimpltarget.lean:26:0-26:7: warning: declaration uses 'sorry'