From 218119fbfad7ca1affc255f4da6ceac123dc1beb Mon Sep 17 00:00:00 2001
From: dmyTRUEk <25669613+dmyTRUEk@users.noreply.github.com>
Date: Thu, 12 Dec 2024 23:49:22 +0200
Subject: [PATCH] fix: missing comma in ch9.Objects

---
 structures_and_records.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/structures_and_records.md b/structures_and_records.md
index b3a0c1c5..664d6a84 100644
--- a/structures_and_records.md
+++ b/structures_and_records.md
@@ -178,9 +178,9 @@ fields were defined. Lean therefore provides the following alternative
 notations for defining elements of a structure type.
 
 ```
-    { (<field-name> := <expr>)* : structure-type }
+    { (<field-name> := <expr>,)* : structure-type }
     or
-    { (<field-name> := <expr>)* }
+    { (<field-name> := <expr>,)* }
 ```
 
 The suffix ``: structure-type`` can be omitted whenever the name of