Zulip Chat Archive

Stream: lean4

Topic: Updating structure fields


view this post on Zulip Calvin Lee (Mar 20 2021 at 17:00):

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?

view this post on Zulip Leonardo de Moura (Mar 20 2021 at 17:03):

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"

view this post on Zulip Calvin Lee (Mar 20 2021 at 17:05):

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

view this post on Zulip Calvin Lee (Mar 20 2021 at 17:06):

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

view this post on Zulip Marc Huisinga (Mar 20 2021 at 17:07):

E.g.

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

view this post on Zulip Andrew Kent (Mar 20 2021 at 21:57):

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}

Last updated: May 18 2021 at 22:15 UTC