From a0fcb660c53362cccc20e9b8455ac75b4f92d0e6 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Tue, 13 Sep 2022 09:19:23 -0400
Subject: [PATCH] feat: allow multiple source + no expected type

---
 src/Lean/Elab/StructInst.lean            | 14 +++++---------
 tests/lean/structInst1.lean              |  9 ++++++++-
 tests/lean/structInst1.lean.expected.out |  3 ++-
 3 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 3e93a9582d..f13b473d52 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/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 =>
diff --git a/tests/lean/structInst1.lean b/tests/lean/structInst1.lean
index 84ba7a193c..970d720191 100644
--- a/tests/lean/structInst1.lean
+++ b/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
diff --git a/tests/lean/structInst1.lean.expected.out b/tests/lean/structInst1.lean.expected.out
index 703e207263..9903d88d86 100644
--- a/tests/lean/structInst1.lean.expected.out
+++ b/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