Updating structure fields

Stream: lean4

[Calvin Lee]

the lean docs have a TODO in the "Updating Structure Fields" section of structure documentation. Does this exist and is undocumented or does it not yet exist?

[Leonardo de Moura]

Calvin Lee said:

the lean docs have a TODO in the "Updating Structure Fields" section of structure documentation. Does this exist and is undocumented or does it not yet exist?

Every "TODO" in the documentation means: "the feature exists but is undocumented"

[Calvin Lee]

Ah, that's what I thought but I wasn't able to find it in the codebase (with some quick grepping) since I don't quite know what the syntax looks like

[Calvin Lee]

What is the syntax (or function) that performs structure "update"?

[Marc Huisinga]

E.g.

let updatedFoo := { foo with fieldToUpdate := updatedValue }

[Andrew Kent]

You can also update nested fields in one go -- it's pretty cool IMO =)

structure Point where
  x : Int
  y : Int

structure Line where
  start : Point
  stop  : Point

def Line.adjustY (n : Int) (l : Line ) : Line :=
  {l with start.y := l.start.y + n,
          stop.y := l.stop.y + n}