From 7ef694b0c31d36351e804ef45c9c052588e391b0 Mon Sep 17 00:00:00 2001
From: Yannick Seurin <yannick.seurin@gmail.com>
Date: Mon, 8 Sep 2025 15:32:15 +0200
Subject: [PATCH] add record syntax for defining a value of structure type

---
 MIL/C07_Structures/S01_Structures.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/MIL/C07_Structures/S01_Structures.lean b/MIL/C07_Structures/S01_Structures.lean
index f9fd6cf..b419445 100644
--- a/MIL/C07_Structures/S01_Structures.lean
+++ b/MIL/C07_Structures/S01_Structures.lean
@@ -50,9 +50,12 @@ def myPoint1 : Point where
   z := 4
 
 def myPoint2 : Point :=
+  { x := 2, y := -1, z := 4 }
+
+def myPoint3 : Point :=
   ⟨2, -1, 4⟩
 
-def myPoint3 :=
+def myPoint4 :=
   Point.mk 2 (-1) 4
 -- QUOTE.
 
@@ -67,7 +70,7 @@ def myPoint3 :=
 
 In the first example, the fields of the structure are named
 explicitly.
-The function ``Point.mk`` referred to in the definition of ``myPoint3``
+The function ``Point.mk`` referred to in the definition of ``myPoint4``
 is known as the *constructor* for the ``Point`` structure, because
 it serves to construct elements.
 You can specify a different name if you want, like ``build``.