feat: allow multiple source + no expected type

src/Lean/Elab/StructInst.lean

@@ -193,15 +193,11 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
 private def getStructName (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
   tryPostponeIfNoneOrMVar expectedType?
   let useSource : Unit → TermElabM Name := fun _ => do
-    match sourceView.explicit.size with
-    | 0 =>
-      match expectedType? with
-      | some expectedType => throwUnexpectedExpectedType expectedType
-      | none => throwUnknownExpectedType
-    | 1 => return sourceView.explicit[0]!.structName
-    | _ =>
-      throwErrorAt sourceView.explicit[1]!.stx
-        "invalid \{...} notation, expected type is not known, using the type of the first source, extra sources are not needed"
+    unless sourceView.explicit.isEmpty do
+      return sourceView.explicit[0]!.structName
+    match expectedType? with
+    | some expectedType => throwUnexpectedExpectedType expectedType
+    | none => throwUnknownExpectedType
   match expectedType? with
   | none => useSource ()
   | some expectedType =>

tests/lean/structInst1.lean

@@ -33,4 +33,11 @@ theorem ex4 (a : A) (c : C) : (f4 c a).x = 0 :=
   rfl
 
 def f5 (c : C) (a : A) :=
-  { c, a with x := 0 } -- Error
+  { c, a with x := 0 }
+
+#check f5
+
+def f6 (c : C) (a : A) :=
+  { a, c with x := 0 }
+
+#check f6

tests/lean/structInst1.lean.expected.out

@@ -1,2 +1,3 @@
 structInst1.lean:12:11-12:19: error: field 'toA' has already beed specified
-structInst1.lean:36:7-36:8: error: invalid {...} notation, expected type is not known, using the type of the first source, extra sources are not needed
+f5 : C → A → C
+f6 : C → A → A