From 1145976ff9dbe6234933f968a8d8bebe4b285319 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 28 Dec 2023 16:28:17 +0100 Subject: [PATCH] =?UTF-8?q?test:=20test=20=E2=80=9Cmotive=20is=20not=20typ?= =?UTF-8?q?e=20correct=E2=80=9D=20(#3122)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- tests/lean/motiveNotTypeCorect.lean | 8 ++++++++ tests/lean/motiveNotTypeCorect.lean.expected.out | 7 +++++++ 2 files changed, 15 insertions(+) create mode 100644 tests/lean/motiveNotTypeCorect.lean create mode 100644 tests/lean/motiveNotTypeCorect.lean.expected.out diff --git a/tests/lean/motiveNotTypeCorect.lean b/tests/lean/motiveNotTypeCorect.lean new file mode 100644 index 0000000000..a999327af0 --- /dev/null +++ b/tests/lean/motiveNotTypeCorect.lean @@ -0,0 +1,8 @@ +inductive D : Nat -> Type +def mwe (t : Nat) (f : Nat -> Nat) (h : f t = t) + (d : D (f t)) + (P : (t : Nat) -> D t -> Prop) + : P (f t) d + := by + rw [h] -- tactic 'rewrite' failed, motive is not type correct + sorry diff --git a/tests/lean/motiveNotTypeCorect.lean.expected.out b/tests/lean/motiveNotTypeCorect.lean.expected.out new file mode 100644 index 0000000000..cee57716ed --- /dev/null +++ b/tests/lean/motiveNotTypeCorect.lean.expected.out @@ -0,0 +1,7 @@ +motiveNotTypeCorect.lean:7:6-7:7: error: tactic 'rewrite' failed, motive is not type correct +t : Nat +f : Nat → Nat +h : f t = t +d : D (f t) +P : (t : Nat) → D t → Prop +⊢ P (f t) d