From b5a434d8a93ee9bbd0d8f14422189b43d8289420 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Aug 2021 11:15:14 -0700 Subject: [PATCH] test: for `induction q with Quot.ind` issue See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Induction.20alternative.20name.20when.20using.20Quot.2Eind.3F --- tests/lean/run/quotInd.lean | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 tests/lean/run/quotInd.lean diff --git a/tests/lean/run/quotInd.lean b/tests/lean/run/quotInd.lean new file mode 100644 index 0000000000..f620e29cd7 --- /dev/null +++ b/tests/lean/run/quotInd.lean @@ -0,0 +1,3 @@ +example (r : α → α → Prop) (q : Quot r) : False := by + induction q using Quot.ind with + | mk x => admit