diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index bfa99d8ef1..d6fef9d23a 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -773,6 +773,17 @@ else
   let stxNew   := stx.setArg 4 mkNullNode;
   `(($stxNew : $expected))
 
+private def isEmptyStructInst (stx : Syntax) : Bool :=
+(stx.getArg 1).isNone &&
+(stx.getArg 2).isNone &&
+(stx.getArg 3).isNone &&
+(stx.getArg 4).isNone
+
+@[builtinTermElab emptyC] def expandEmptyC : TermElab :=
+fun stx expectedType? => do
+  stxNew ← `(HasEmptyc.emptyc);
+  withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+
 @[builtinTermElab structInst] def elabStructInst : TermElab :=
 fun stx expectedType? => do
   stxNew? ← liftMacroM $ expandStructInstExpectedType stx;
@@ -784,11 +795,22 @@ fun stx expectedType? => do
     | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
     | none => do
       sourceView ← getStructSource stx;
-      modifyOp?  ← isModifyOp? stx;
-      match modifyOp?, sourceView with
-      | some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
-      | some _,        _                        => throwError ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
-      | _,             _                        => elabStructInstAux stx expectedType? sourceView
+      if isEmptyStructInst stx then do
+        /- Recall that we also want to use `{}` as notation for `HasEmptyc.emptyc` -/
+        tryPostponeIfNoneOrMVar expectedType?;
+        match expectedType? with
+        | none => expandEmptyC stx expectedType?
+        | some expectedType =>
+          /- We first try to create `@HasEmptyc.emptyc expectedType _`, if it fails, we elaborate as the empty structure. -/
+          catch
+            (mkAppOptM `HasEmptyc.emptyc #[expectedType, none])
+            (fun _ => elabStructInstAux stx expectedType? sourceView)
+      else do
+        modifyOp?  ← isModifyOp? stx;
+        match modifyOp?, sourceView with
+        | some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
+        | some _,        _                        => throwError ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
+        | _,             _                        => elabStructInstAux stx expectedType? sourceView
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Elab.struct;
diff --git a/tests/lean/run/emptyc.lean b/tests/lean/run/emptyc.lean
new file mode 100644
index 0000000000..1e477ac9c2
--- /dev/null
+++ b/tests/lean/run/emptyc.lean
@@ -0,0 +1,22 @@
+new_frontend
+
+structure A :=
+(x : Nat := 0)
+
+def foo : A :=
+{}
+
+theorem ex1 : foo = { x := 0 } :=
+rfl
+
+theorem ex2 : foo.x = 0 :=
+rfl
+
+instance : HasEmptyc A :=
+⟨{ x := 10 }⟩
+
+def boo : A :=
+{} -- this HasEmptyc.emptyc
+
+theorem ex3 : boo.x = 10 :=
+rfl