Zulip Chat Archive

Stream: new members

Topic: with or ..

Joachim Breitner (Feb 15 2022 at 13:16):

Is there a difference between { foo with bar := baz, } and {bar := baz, ..foo}?

Eric Wieser (Feb 15 2022 at 13:17):

I think only the latter syntax lets you unpack multiple structures

Eric Wieser (Feb 15 2022 at 13:17):

Maybe there's more to it though

Reid Barton (Feb 15 2022 at 13:24):

According to my grep attempt, mathlib only uses the former a few times in tactics

Reid Barton (Feb 15 2022 at 13:24):

I didn't know it existed

Joachim Breitner (Feb 15 2022 at 13:30):

I find slightly odd that the .. syntax is preferred, when the { foo with …} is (IMHO) more readable and natural: You start with the object you want to extend, and then you list the additional fields.
But maybe uniformity is useful, and so with really shouldn’t be used in mathlib?

Joachim Breitner (Feb 15 2022 at 13:33):

The reference manual at <https://leanprover.github.io/reference/declarations.html#structures-and-records> doesn't give much guidance. Although unless I am blind it only documents with, but not ..foo syntax?

Yaël Dillies (Feb 15 2022 at 13:34):

I personally didn't even know this syntax existed.

Adam Topaz (Feb 15 2022 at 13:39):

Does { foo with ... } work when you want to have multiple foos?

Adam Topaz (Feb 15 2022 at 13:39):


structure foo :=
(a : )

structure bar extends foo :=
(b : )

structure baz :=
(a : )
(b : )
(c : )

example (f : foo) (g : bar) (c : ) : baz :=
{ c := c, .. f, .. g }

Adam Topaz (Feb 15 2022 at 13:40):

There might be some way to do this with the { foo with ... } syntax, but I don't know what it is.

Joachim Breitner (Feb 15 2022 at 13:54):

Sounds like the .. is more versatile and powerful, and conversely with simpler?

Reid Barton (Feb 15 2022 at 14:53):

Maybe there is a difference in intention (even if not technically, not sure): { x with a := t' } suggests we already have a structure of the same type and we are changing one of the fields, while { b := u, .. x } suggests that we are building a bigger structure reusing some fields from x.

Reid Barton (Feb 15 2022 at 14:54):

The first one would be relatively rare in math (for instance if the structure is a proposition, then it makes no sense).

Joachim Breitner (Feb 15 2022 at 15:19):

Hmm, in a language with extensible records I am not surprised that with allows extension, not just updates. But I see your point.

Is {.. x, b := u} legal? (On the phone right now)

Alex J. Best (Feb 15 2022 at 15:25):

It's not legal it seems

Yaël Dillies (Feb 15 2022 at 15:37):

The thing is that the .. fill in everything they can as soon as they're used. So you want to use them last.

Joachim Breitner (Feb 15 2022 at 15:37):

Isnt that odd? I can out a .. foo before.. bar, but not before individual field assignments? Anyways, probably all not so important, and I'll adjust to the mathlib style

Yaël Dillies (Feb 15 2022 at 15:38):

Are you using the old or new structure command? What is the value of old_structure_cmd?

Yaël Dillies (Feb 15 2022 at 15:40):

If you're using the new one, then usually what you consider a single field of a structure is actually a field of a parent one and the structure you have in hand has that parent as a field. If you understand this, then you'll see why the { := , := } is such a nice syntax sugar.

Kyle Miller (Feb 15 2022 at 19:39):

I thought I had remembered Mario discussing with vs .. and the history of .. in Lean 3, but all I managed to dig up was https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.22.2E.2Es.22.20in.20structure.20literals/near/224902754

Too bad "with" is a stop word for Zulip's search...

Mario Carneiro (Feb 16 2022 at 04:20):

By the way for the curious, the ..s notation has since been added as a mathlib4 extension written __ := s. I think it is also less restrictive in terms of its positioning wrt other fields

Last updated: Dec 20 2023 at 11:08 UTC