From 87d3961158f0f7811fa2d4ace9498b427d0cc1b9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Sep 2013 13:21:57 -0700 Subject: [PATCH] Improve elaborator error messages Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_elaborator.cpp | 113 ++++++++++++++---- src/frontends/lean/lean_elaborator.h | 2 + .../lean/lean_elaborator_exception.cpp | 70 ++++++++++- .../lean/lean_elaborator_exception.h | 24 +++- src/frontends/lean/lean_pp.cpp | 2 +- src/kernel/level.cpp | 2 +- src/library/formatter.cpp | 7 +- src/tests/frontends/lean/implicit_args.cpp | 9 +- src/util/sexpr/format.cpp | 4 +- tests/lean/elab1.lean | 29 +++++ tests/lean/elab1.lean.expected.out | 81 +++++++++++++ tests/lean/tst7.lean.expected.out | 7 +- 12 files changed, 310 insertions(+), 40 deletions(-) create mode 100644 tests/lean/elab1.lean create mode 100644 tests/lean/elab1.lean.expected.out diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index 5155109bc..f3f979c72 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -46,20 +46,65 @@ expr const & get_choice(expr const & e, unsigned i) { } class elaborator::imp { + // Information for producing error messages regarding application type mismatch during elaboration + struct app_mismatch_info { + expr m_app; // original application + context m_ctx; // context where application occurs + std::vector m_args; // arguments after processing + std::vector m_types; // inferred types of the arguments + app_mismatch_info(expr const & app, context const & ctx, unsigned sz, expr const * args, expr const * types): + m_app(app), m_ctx(ctx), m_args(args, args+sz), m_types(types, types+sz) {} + }; + + // Information for producing error messages regarding expected type mismatch during elaboration + struct expected_type_info { + expr m_expr; // original expression + expr m_processed_expr; // expression after processing + expr m_expected; // expected type + expr m_given; // inferred type of the processed expr. + context m_ctx; + expected_type_info(expr const & e, expr const & p, expr const & exp, expr const & given, context const & ctx): + m_expr(e), m_processed_expr(p), m_expected(exp), m_given(given), m_ctx(ctx) {} + }; + + enum class info_kind { AppMismatchInfo, ExpectedTypeInfo }; + + typedef std::pair info_ref; + + std::vector m_app_mismatch_info; + std::vector m_expected_type_info; + + info_ref mk_app_mismatch_info(expr const & app, context const & ctx, unsigned sz, expr const * args, expr const * types) { + unsigned idx = m_app_mismatch_info.size(); + m_app_mismatch_info.push_back(app_mismatch_info(app, ctx, sz, args, types)); + return mk_pair(info_kind::AppMismatchInfo, idx); + } + + info_ref mk_expected_type_info(expr const & e, expr const & p, expr const & exp, expr const & g, context const & ctx) { + unsigned idx = m_expected_type_info.size(); + m_expected_type_info.push_back(expected_type_info(e, p, exp, g, ctx)); + return mk_pair(info_kind::ExpectedTypeInfo, idx); + } + + context get_context(info_ref const & r) const { + if (r.first == info_kind::AppMismatchInfo) + return m_app_mismatch_info[r.second].m_ctx; + else + return m_expected_type_info[r.second].m_ctx; + } + // unification constraint lhs == second struct constraint { expr m_lhs; expr m_rhs; context m_ctx; - expr m_source; // auxiliary field used for producing error msgs - context m_source_ctx; // auxiliary field used for producing error msgs - unsigned m_arg_pos; // auxiliary field used for producing error msgs - constraint(expr const & lhs, expr const & rhs, context const & ctx, expr const & src, context const & src_ctx, unsigned arg_pos): - m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(src), m_source_ctx(src_ctx), m_arg_pos(arg_pos) {} + info_ref m_info; + constraint(expr const & lhs, expr const & rhs, context const & ctx, info_ref const & r): + m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_info(r) {} constraint(expr const & lhs, expr const & rhs, constraint const & c): - m_lhs(lhs), m_rhs(rhs), m_ctx(c.m_ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {} + m_lhs(lhs), m_rhs(rhs), m_ctx(c.m_ctx), m_info(c.m_info) {} constraint(expr const & lhs, expr const & rhs, context const & ctx, constraint const & c): - m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {} + m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_info(c.m_info) {} }; // information associated with the metavariable @@ -331,7 +376,8 @@ class elaborator::imp { expr expected = abst_domain(f_t); expr given = types[i]; if (has_metavar(expected) || has_metavar(given)) { - m_constraints.push_back(constraint(expected, given, ctx, e, ctx, i)); + info_ref r = mk_app_mismatch_info(e, ctx, args.size(), args.data(), types.data()); + m_constraints.push_back(constraint(expected, given, ctx, r)); } else { if (!is_convertible(expected, given, ctx)) { expr coercion = m_frontend.get_coercion(given, expected); @@ -439,10 +485,21 @@ class elaborator::imp { [[noreturn]] void throw_unification_exception(constraint const & c) { // display(std::cout); m_constraints.push_back(c); - if (c.m_arg_pos != static_cast(-1)) { - throw unification_app_mismatch_exception(*m_owner, c.m_source_ctx, c.m_source, c.m_arg_pos); + info_ref const & r = c.m_info; + if (r.first == info_kind::AppMismatchInfo) { + app_mismatch_info & info = m_app_mismatch_info[r.second]; + for (expr & arg : info.m_args) + arg = instantiate(arg); + for (expr & type : info.m_types) + type = instantiate(type); + throw unification_app_mismatch_exception(*m_owner, info.m_ctx, info.m_app, info.m_args, info.m_types); } else { - throw unification_type_mismatch_exception(*m_owner, c.m_source_ctx, c.m_source); + expected_type_info & info = m_expected_type_info[r.second]; + info.m_processed_expr = instantiate(info.m_processed_expr); + info.m_given = instantiate(info.m_given); + info.m_expected = instantiate(info.m_expected); + throw unification_type_mismatch_exception(*m_owner, info.m_ctx, info.m_expr, info.m_processed_expr, + info.m_expected, info.m_given); } } @@ -651,25 +708,31 @@ class elaborator::imp { cont = true; // must continue } else { if (m_metavars[midx].m_type && !m_metavars[midx].m_type_cnstr) { + context ctx = m_metavars[midx].m_ctx; try { - expr t = infer(m_metavars[midx].m_assignment, m_metavars[midx].m_ctx); + expr t = infer(m_metavars[midx].m_assignment, ctx); m_metavars[midx].m_type_cnstr = true; - m_constraints.push_back(constraint(m_metavars[midx].m_type, t, m_metavars[midx].m_ctx, - m_metavars[midx].m_mvar, m_metavars[midx].m_ctx, static_cast(-1))); + info_ref r = mk_expected_type_info(m_metavars[midx].m_mvar, m_metavars[midx].m_mvar, + m_metavars[midx].m_type, t, ctx); + m_constraints.push_back(constraint(m_metavars[midx].m_type, t, ctx, r)); progress = true; } catch (exception&) { // std::cout << "Failed to infer type of: ?M" << midx << "\n" // << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n"; - throw unification_type_mismatch_exception(*m_owner, m_metavars[midx].m_ctx, m_metavars[midx].m_mvar); + expr null_given_type; // failed to infer given type. + throw unification_type_mismatch_exception(*m_owner, ctx, m_metavars[midx].m_mvar, m_metavars[midx].m_mvar, + m_metavars[midx].m_type, null_given_type); } } } + } else { + cont = true; } } if (!cont) return; if (!progress) - throw unsolved_placeholder_exception(*m_owner, context(), m_root); + return; } } @@ -716,20 +779,27 @@ public: } expr operator()(expr const & e, expr const & expected_type, elaborator const & elb) { + m_owner = &elb; m_constraints.clear(); m_metavars.clear(); - m_owner = &elb; + m_app_mismatch_info.clear(); + m_expected_type_info.clear(); m_processing_root = true; auto p = process(e, context()); m_root = p.first; expr given_type = p.second; if (expected_type) { - if (has_metavar(given_type)) - m_constraints.push_back(constraint(expected_type, given_type, context(), e, context(), static_cast(-1))); + if (has_metavar(given_type)) { + info_ref r = mk_expected_type_info(e, m_root, expected_type, given_type, context()); + m_constraints.push_back(constraint(expected_type, given_type, context(), r)); + } } if (has_metavar(m_root)) { solve(); - return instantiate(m_root); + expr r = instantiate(m_root); + if (has_metavar(r)) + throw unsolved_placeholder_exception(elb, context(), m_root); + return r; } else { return m_root; } @@ -756,6 +826,8 @@ public: } return r; } + + bool has_constraints() const { return !m_constraints.empty(); } }; elaborator::elaborator(frontend const & fe):m_ptr(new imp(fe, nullptr)) {} elaborator::~elaborator() {} @@ -768,4 +840,5 @@ environment const & elaborator::get_environment() const { return m_ptr->get_envi void elaborator::display(std::ostream & out) const { m_ptr->display(out); } format elaborator::pp(formatter & f, options const & o) const { return m_ptr->pp(f,o); } void elaborator::print(imp * ptr) { ptr->display(std::cout); } +bool elaborator::has_constraints() const { return m_ptr->has_constraints(); } } diff --git a/src/frontends/lean/lean_elaborator.h b/src/frontends/lean/lean_elaborator.h index 1937f92ea..fd3ed8844 100644 --- a/src/frontends/lean/lean_elaborator.h +++ b/src/frontends/lean/lean_elaborator.h @@ -44,6 +44,8 @@ public: void display(std::ostream & out) const; format pp(formatter & f, options const & o) const; + + bool has_constraints() const; }; /** \brief Create a choice expression for the given functions. diff --git a/src/frontends/lean/lean_elaborator_exception.cpp b/src/frontends/lean/lean_elaborator_exception.cpp index 8e9497d7e..d96cdc26f 100644 --- a/src/frontends/lean/lean_elaborator_exception.cpp +++ b/src/frontends/lean/lean_elaborator_exception.cpp @@ -21,6 +21,17 @@ format pp(formatter fmt, context const & ctx, std::vector const & exprs, s return r; } +format pp_elaborator_state(formatter fmt, elaborator const & elb, options const & opts) { + unsigned indent = get_pp_indent(opts); + format r; + if (elb.has_constraints()) { + format elb_fmt = elb.pp(fmt, opts); + r += compose(line(), format("Elaborator state")); + r += nest(indent, compose(line(), elb_fmt)); + } + return r; +} + format pp(formatter fmt, elaborator_exception const & ex, options const & opts) { unsigned indent = get_pp_indent(opts); context const & ctx = ex.get_context(); @@ -31,13 +42,60 @@ format pp(formatter fmt, elaborator_exception const & ex, options const & opts) r += format{line(), format("Arguments:")}; r += pp(fmt, ctx, _ex->get_args(), _ex->get_arg_types(), opts); return r; + } else if (unification_app_mismatch_exception const * _ex = dynamic_cast(&ex)) { + unsigned indent = get_pp_indent(opts); + auto const & elb = _ex->get_elaborator(); + auto const & ctx = _ex->get_context(); + expr const & app = _ex->get_expr(); + auto const & args = _ex->get_args(); + auto const & types = _ex->get_types(); + auto args_it = args.begin(); + auto types_it = types.begin(); + format app_fmt = fmt(ctx, app, false, opts); + format r = format{format(_ex->what()), nest(indent, compose(line(), app_fmt))}; + format fun_type_fmt = fmt(ctx, *types_it, false, opts); + r += compose(line(), format("Function type:")); + r += nest(indent, compose(line(), fun_type_fmt)); + ++args_it; + ++types_it; + if (args.size() > 2) + r += compose(line(), format("Arguments types:")); + else + r += compose(line(), format("Argument type:")); + for (; args_it != args.end(); ++args_it, ++types_it) { + format arg_fmt = fmt(ctx, *args_it, false, opts); + format type_fmt = fmt(ctx, *types_it, false, opts); + r += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), type_fmt})}))); + } + r += pp_elaborator_state(fmt, elb, opts); + return r; + } else if (unification_type_mismatch_exception const * _ex = dynamic_cast(&ex)) { + unsigned indent = get_pp_indent(opts); + auto const & elb = _ex->get_elaborator(); + auto const & ctx = _ex->get_context(); + expr const & e = _ex->get_expr(); + expr const & p = _ex->get_processed_expr(); + expr const & exp = _ex->get_expected_type(); + expr const & given = _ex->get_given_type(); + format r = format{format(_ex->what()), nest(indent, compose(line(), fmt(ctx, e, false, opts)))}; + if (p != e) { + r += compose(line(), format("Term after elaboration:")); + r += nest(indent, compose(line(), fmt(ctx, p, false, opts))); + } + r += compose(line(), format("Expected type:")); + r += nest(indent, compose(line(), fmt(ctx, exp, false, opts))); + if (given) { + r += compose(line(), format("Got:")); + r += nest(indent, compose(line(), fmt(ctx, given, false, opts))); + } + r += pp_elaborator_state(fmt, elb, opts); + return r; } else { - format expr_f = fmt(ctx, ex.get_expr(), false, opts); - format elb_f = ex.get_elaborator().pp(fmt, opts); - return format({format(ex.what()), space(), format("at term"), - nest(indent, compose(line(), expr_f)), - line(), format("Elaborator state"), - nest(indent, compose(line(), elb_f))}); + auto const & elb = ex.get_elaborator(); + format expr_fmt = fmt(ctx, ex.get_expr(), false, opts); + format r = format{format(ex.what()), space(), format("at term"), nest(indent, compose(line(), expr_fmt))}; + r += pp_elaborator_state(fmt, elb, opts); + return r; } } diff --git a/src/frontends/lean/lean_elaborator_exception.h b/src/frontends/lean/lean_elaborator_exception.h index 1c3b8601a..b580426f2 100644 --- a/src/frontends/lean/lean_elaborator_exception.h +++ b/src/frontends/lean/lean_elaborator_exception.h @@ -42,16 +42,32 @@ public: }; class unification_app_mismatch_exception : public elaborator_exception { - unsigned m_arg_pos; + std::vector m_args; + std::vector m_types; public: - unification_app_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s, unsigned pos):elaborator_exception(elb, ctx, s), m_arg_pos(pos) {} - unsigned get_arg_pos() const { return m_arg_pos; } + unification_app_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s, + std::vector const & args, std::vector const & types): + elaborator_exception(elb, ctx, s), + m_args(args), + m_types(types) {} + virtual ~unification_app_mismatch_exception() {} + std::vector const & get_args() const { return m_args; } + std::vector const & get_types() const { return m_types; } virtual char const * what() const noexcept { return "application type mismatch during term elaboration"; } }; class unification_type_mismatch_exception : public elaborator_exception { + expr m_processed_expr; + expr m_expected_type; + expr m_given_type; public: - unification_type_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s):elaborator_exception(elb, ctx, s) {} + unification_type_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s, + expr const & processed, expr const & expected, expr const & given): + elaborator_exception(elb, ctx, s), m_processed_expr(processed), m_expected_type(expected), m_given_type(given) {} + virtual ~unification_type_mismatch_exception() {} + expr const & get_processed_expr() const { return m_processed_expr; } + expr const & get_expected_type() const { return m_expected_type; } + expr const & get_given_type() const { return m_given_type; } virtual char const * what() const noexcept { return "type mismatch during term elaboration"; } }; diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp index 4900f9672..ec5f0ede8 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -247,7 +247,7 @@ class pp_fn { // expression, but an alias is created for it. return r; } else { - return mk_result(format{lp(), nest(1, format{r.first, rp()})}, r.second); + return mk_result(paren(r.first), r.second); } } diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index c886bc051..35a0160c3 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -219,7 +219,7 @@ format pp(level const & l, bool unicode) { format r = format("max"); for (unsigned i = 0; i < max_size(l); i++) r += format{line(), pp(max_level(l, i), unicode)}; - return group(nest(1, format{lp(), r, rp()})); + return paren(r); } }} lean_unreachable(); diff --git a/src/library/formatter.cpp b/src/library/formatter.cpp index 034e182d2..41cf0dd6b 100644 --- a/src/library/formatter.cpp +++ b/src/library/formatter.cpp @@ -43,7 +43,7 @@ format formatter::operator()(kernel_exception const & ex, options const & opts) return format{format("invalid object declaration, environment already has an object named '"), format(_ex->get_name()), format("'")}; } else if (app_type_mismatch_exception const * _ex = dynamic_cast(&ex)) { - unsigned indent = get_pp_indent(opts); + unsigned indent = get_pp_indent(opts); context const & ctx = _ex->get_context(); expr const & app = _ex->get_application(); format app_fmt = operator()(ctx, app, false, opts); @@ -53,7 +53,10 @@ format formatter::operator()(kernel_exception const & ex, options const & opts) format arg_types_fmt; ++it; for (unsigned i = 1; it != arg_types.end(); ++it, ++i) { - format arg_fmt = operator()(ctx, arg(app, i), false, opts); + expr const & a = arg(app, i); + format arg_fmt = operator()(ctx, a, false, opts); + if (is_pi(a) || is_lambda(a) || is_let(a)) + arg_fmt = paren(arg_fmt); format arg_type_fmt = operator()(ctx, *it, false, opts); arg_types_fmt += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), arg_type_fmt})}))); } diff --git a/src/tests/frontends/lean/implicit_args.cpp b/src/tests/frontends/lean/implicit_args.cpp index e84fa3488..c67df1f9a 100644 --- a/src/tests/frontends/lean/implicit_args.cpp +++ b/src/tests/frontends/lean/implicit_args.cpp @@ -30,7 +30,7 @@ static void success(expr const & e, expr const & expected, frontend const & env) try { std::cout << elaborate(e, env) << "\n"; } catch (unification_app_mismatch_exception & ex) { - std::cout << "Error at argumet " << ex.get_arg_pos() << " of " << mk_pair(ex.get_expr(), ex.get_context()) << "\n"; + std::cout << "Error at " << mk_pair(ex.get_expr(), ex.get_context()) << "\n"; } catch (unification_type_mismatch_exception & ex) { std::cout << "Error at " << mk_pair(ex.get_expr(), ex.get_context()) << " " << ex.what() << "\n"; std::cout << "Elaborator:\n"; ex.get_elaborator().display(std::cout); std::cout << "-----------------\n"; @@ -58,8 +58,11 @@ static void fails(expr const & e, frontend const & env) { // Check elaborator partial success (i.e., result still contain some metavariables */ static void unsolved(expr const & e, frontend const & env) { - std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n"; - lean_assert(has_metavar(elaborate(e, env))); + try { + std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n"; + lean_unreachable(); + } catch (unsolved_placeholder_exception) { + } } #define _ mk_placholder() diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 79c908fd3..0f52834f2 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -216,7 +216,7 @@ format bracket(std::string const l, format const & x, std::string const r) { format(r)}); } format paren(format const & x) { - return bracket("(", x, ")"); + return group(nest(1, format{lp(), x, rp()})); } // wrap = <+/> @@ -415,7 +415,7 @@ struct sexpr_pp_fn { r += apply(head(*curr)); curr = &tail(*curr); if (is_nil(*curr)) { - return group(nest(1, format{lp(), r, rp()})); + return paren(r); } else if (!is_cons(*curr)) { return group(nest(1, format{lp(), r, space(), dot(), line(), apply(*curr), rp()})); } else { diff --git a/tests/lean/elab1.lean b/tests/lean/elab1.lean new file mode 100644 index 000000000..e66f34937 --- /dev/null +++ b/tests/lean/elab1.lean @@ -0,0 +1,29 @@ + + +Variable f {A : Type} (a b : A) : A. +Check f 10 true + +Variable g {A B : Type} (a : A) : A. +Check g 10 + +Variable h : Pi (A : Type), A -> A. + +Check fun x, fun A : Type, h A x + +Variable eq : Pi A : Type, A -> A -> Bool. + +Check fun (A B : Type) (a : _) (b : _) (C : Type), eq C a b. + +Variable a : Bool +Variable b : Bool +Variable H : a /\ b +Theorem t1 : b := Discharge (fun H1, Conj H1 (Conjunct1 H)). + +Theorem t2 : a = b := Trans (Refl a) (Refl b). + +Check f Bool Bool. + +Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a := + Discharge (λ H, DisjCases (EM a) + (λ H_a, H) + (λ H_na, NotImp1 (MT H H_na))) diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out new file mode 100644 index 000000000..38bc9ae28 --- /dev/null +++ b/tests/lean/elab1.lean.expected.out @@ -0,0 +1,81 @@ + Set: pp::colors + Set: pp::unicode + Assumed: f +Error (line: 4, pos: 6) type mismatch at application + f 10 ⊤ +Function type: + Π (A : Type) (a b : A), A +Arguments types: + ℕ : Type + 10 : ℕ + ⊤ : Bool + Assumed: g +Error (line: 7, pos: 6) unsolved placeholder at term + g 10 + Assumed: h +Error (line: 11, pos: 27) application type mismatch during term elaboration + h A x +Function type: + Π (A : Type) (_ : A), A +Arguments types: + A : Type + x : lift:0:2 ?M0 +Elaborator state + #0 ≈ lift:0:2 ?M0 + Assumed: eq +Error (line: 15, pos: 51) application type mismatch during term elaboration + eq C a b +Function type: + Π (A : Type) (_ _ : A), Bool +Arguments types: + C : Type + a : lift:0:3 ?M0 + b : lift:0:2 ?M2 +Elaborator state + #0 ≈ lift:0:2 ?M2 + #0 ≈ lift:0:3 ?M0 + Assumed: a + Assumed: b + Assumed: H +Error (line: 20, pos: 18) type mismatch during term elaboration + Discharge (λ H1 : _, Conj H1 (Conjunct1 H)) +Term after elaboration: + Discharge (λ H1 : ?M4, Conj H1 (Conjunct1 H)) +Expected type: + b +Got: + ?M4 ⇒ ?M2 +Elaborator state + lift:0:1 ?M2 ≈ lift:0:1 ?M4 ∧ a + b ≈ if Bool ?M4 ?M2 ⊤ + b ≈ if Bool ?M4 ?M2 ⊤ +Error (line: 22, pos: 22) type mismatch at application + Trans (Refl a) (Refl b) +Function type: + Π (A : Type U) (a b c : A) (H1 : a = b) (H2 : b = c), a = c +Arguments types: + Bool : Type + a : Bool + a : Bool + b : Bool + Refl a : a = a + Refl b : b = b +Error (line: 24, pos: 6) type mismatch at application + f Bool Bool +Function type: + Π (A : Type) (a b : A), A +Arguments types: + Type : Type 1 + Bool : Type + Bool : Type +Error (line: 27, pos: 21) type mismatch at application + DisjCases (EM a) (λ H_a : a, H) (λ H_na : ¬ a, NotImp1 (MT H H_na)) +Function type: + Π (a b c : Bool) (H1 : a ∨ b) (H2 : a → c) (H3 : b → c), c +Arguments types: + a : Bool + ¬ a : Bool + a : Bool + EM a : a ∨ ¬ a + (λ H_a : a, H) : a → ((a ⇒ b) ⇒ a) + (λ H_na : ¬ a, NotImp1 (MT H H_na)) : (¬ a) → a diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out index 74a88fbea..c58424943 100644 --- a/tests/lean/tst7.lean.expected.out +++ b/tests/lean/tst7.lean.expected.out @@ -2,8 +2,13 @@ Set: pp::unicode Assumed: f λ (A B : Type) (a : B), f B a -Error (line: 4, pos: 40) application type mismatch during term elaboration at term +Error (line: 4, pos: 40) application type mismatch during term elaboration f B a +Function type: + Π (A : Type) (_ : A), Bool +Arguments types: + B : Type + a : lift:0:2 ?M0 Elaborator state #0 ≈ lift:0:2 ?M0 Assumed: myeq