From 3aa5ebb8bdef50b06dc8ad25a4366a8e578caf9e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 1 Sep 2017 14:04:19 +0200 Subject: [PATCH] feat(frontends/lean/elaborator): structure notation: allow explicit ctor param when given expected type --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3c5edc1aed..498c84dafb 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2920,7 +2920,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional const & expr c_arg; expr d = binding_domain(c_type); if (i < nparams) { - if (is_explicit(binding_info(c_type))) { + if (is_explicit(binding_info(c_type)) && !expected_type) { report_or_throw(elaborator_exception(e, sstream() << "invalid structure value {...}, structure parameter '" << binding_name(c_type) << "' is explicit in the structure constructor '" <<