feat(frontends/lean/brackets): closes #1820

doc/changes.md

@@ -3,6 +3,8 @@ master branch (aka work in progress branch)
 
 *Features*
 
+- Implemented [RFC #1820](https://github.com/leanprover/lean/issues/1820)
+
 *Changes*
 
 *API name changes*

src/frontends/lean/brackets.cpp

@@ -113,8 +113,16 @@ static expr parse_structure_instance(parser & p, name const & fname) {
 
 /* Parse rest of the structure instance update '{' expr 'with' ... */
 static expr parse_structure_instance_update(parser & p, expr const & e) {
-    name fname = p.check_id_next("invalid structure update, identifier expected");
-    return parse_structure_instance_core(p, some_expr(e), name(), fname);
+    if (p.curr_is_token(get_rcurly_tk())) {
+        // '{' expr 'with' '}'
+        p.next();
+        buffer<name> fns;
+        buffer<expr> fvs;
+        return mk_structure_instance(e, fns, fvs);
+    } else {
+        name fname = p.check_id_next("invalid structure update, identifier expected");
+        return parse_structure_instance_core(p, some_expr(e), name(), fname);
+    }
 }
 
 static name * g_emptyc_or_emptys = nullptr;

tests/lean/run/1820.lean

@@ -0,0 +1,12 @@
+def f (p : nat × nat) : nat × nat := {p with}
+
+structure P (A : Type) extends prod A A :=
+(third : A)
+
+def g (s : P nat) : nat × nat := {s with}
+
+example : g (P.mk (1, 2) 3) = (1, 2) :=
+rfl
+
+example : g ⟨⟨1, 2⟩, 3⟩ = (1, 2) :=
+rfl