From e94095cdf3dd72e24bbea52ba809a43ad6914734 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 18 Jul 2017 09:04:47 +0100 Subject: [PATCH] chore(library/tactic/cases_tactic): add a bit more information to error message --- src/library/tactic/cases_tactic.cpp | 5 ++--- tests/lean/cases_unsupported_equality.lean | 6 ++++++ tests/lean/cases_unsupported_equality.lean.expected.out | 9 +++++++++ 3 files changed, 17 insertions(+), 3 deletions(-) create mode 100644 tests/lean/cases_unsupported_equality.lean create mode 100644 tests/lean/cases_unsupported_equality.lean.expected.out diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index b65b634c87..247b97b3ed 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -440,9 +440,8 @@ struct cases_tactic_fn { auto s = mk_tactic_state(mvar); throw cases_tactic_exception { tactic::mk_exception([=] () { - return format("cases tactic failed, unsupported equality") + line() - + format("(only equalities between constructors and/or variables are") + line() - + format("supported, try cases on the indices):") + line() + return format("cases tactic failed, unsupported equality between type and constructor indices") + line() + + format("(only equalities between constructors and/or variables are supported, try cases on the indices):") + line() + s.pp_expr(H_type) + line(); }, s) }; diff --git a/tests/lean/cases_unsupported_equality.lean b/tests/lean/cases_unsupported_equality.lean new file mode 100644 index 0000000000..d69e75de9e --- /dev/null +++ b/tests/lean/cases_unsupported_equality.lean @@ -0,0 +1,6 @@ +inductive foo : ℕ → Type +| a : foo 0 +| b : ∀ n, foo (n+1) + +example (n) (f : ℕ → ℕ) (h : foo (f n)) : true := +by cases h \ No newline at end of file diff --git a/tests/lean/cases_unsupported_equality.lean.expected.out b/tests/lean/cases_unsupported_equality.lean.expected.out new file mode 100644 index 0000000000..1129dd63b3 --- /dev/null +++ b/tests/lean/cases_unsupported_equality.lean.expected.out @@ -0,0 +1,9 @@ +cases_unsupported_equality.lean:6:3: error: cases tactic failed, unsupported equality between type and constructor indices +(only equalities between constructors and/or variables are supported, try cases on the indices): +f n = 0 + +state: +n : ℕ, +f : ℕ → ℕ, +h : foo (f n) +⊢ f n = 0 → h == foo.a → true