From 37982c6d5c6959fb371e1e1220728582069fb471 Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Wed, 15 Dec 2021 17:18:46 +0530
Subject: [PATCH] doc: structure update

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
---
 doc/struct.md | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/doc/struct.md b/doc/struct.md
index 6c36335aee..695f90214f 100644
--- a/doc/struct.md
+++ b/doc/struct.md
@@ -217,4 +217,11 @@ def msg2 : MessageExt where
 
 ## Updating structure fields
 
-TODO
\ No newline at end of file
+Structure fields can be updated using `{ <struct-val> with <field> := <new-value>, ... }`:
+
+```lean
+# structure Point (α : Type u) where
+#  x : α
+#  y : α
+def incrementX (p : Point Nat) : Point Nat := { p with x := p.x + 1 }
+```