From 9ed678d80ae137fd751587dce230ce6004e2c436 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 1 Sep 2017 14:05:44 +0200
Subject: [PATCH] feat(frontends/lean/elaborator): structure notation:
 synthesize instance-implicit fields

---
 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 498c84dafb..27940854f2 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2996,7 +2996,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
                         report_or_throw(elaborator_exception(e, sstream() << "invalid structure value {...}, field '"
                                                                 << S_fname << "' is implicit and must not be provided"));
                     }
-                    c_arg = mk_metavar(d, ref);
+                    c_arg = binding_info(c_type).is_inst_implicit() ? mk_instance(d, ref) : mk_metavar(d, ref);
                 }
             }
             c_args.push_back(c_arg);