From a544d32fcfc01ebc409a5f2985bb87846e0facba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 26 Oct 2014 16:11:58 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders --- src/frontends/lean/elaborator.cpp | 2 +- tests/lean/pstate.lean | 4 ++++ tests/lean/pstate.lean.expected.out | 5 +++++ 3 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 tests/lean/pstate.lean create mode 100644 tests/lean/pstate.lean.expected.out diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b2d14a51a3..eab2e50cb6 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1035,7 +1035,7 @@ void elaborator::display_unassigned_mvars(expr const & e, substitution const & s expr meta = tmp_s.instantiate(*it); expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first); goal g(meta, meta_type); - proof_state ps(goals(g), substitution(), m_ngen, constraints()); + proof_state ps(goals(g), s, m_ngen, constraints()); display_unsolved_proof_state(e, ps, "don't know how to synthesize it"); } return false; diff --git a/tests/lean/pstate.lean b/tests/lean/pstate.lean new file mode 100644 index 0000000000..0f0dc69a8c --- /dev/null +++ b/tests/lean/pstate.lean @@ -0,0 +1,4 @@ +import logic + +theorem foo {A : Type} (a b c : A) : a = b → b = c → a = c := +assume h₁ h₂, eq.trans h₁ _ diff --git a/tests/lean/pstate.lean.expected.out b/tests/lean/pstate.lean.expected.out new file mode 100644 index 0000000000..1a7180c09b --- /dev/null +++ b/tests/lean/pstate.lean.expected.out @@ -0,0 +1,5 @@ +pstate.lean:4:26: error: unsolved placeholder, don't know how to synthesize it +A : Type, a : A, b : A, c : A, h₁ : a = b, h₂ : b = c ⊢ b = c +pstate.lean:4:7: error: failed to add declaration 'foo' to environment, value has metavariables + λ (A : Type) (a b c : A) (h₁ : a = b) (h₂ : b = c), + eq.trans h₁ ?M_1