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 `{ with := , ... }`: + +```lean +# structure Point (α : Type u) where +# x : α +# y : α +def incrementX (p : Point Nat) : Point Nat := { p with x := p.x + 1 } +```