Nested structure delaborator

Stream: lean4

[Patrick Massot]

This is asking for community feedback before opening a Lean 4 RFC. Consider the following code:

structure A where
  x : Nat

structure B extends A where
  y : Nat

#check ({ x := 1, y := 2 } : B)       --    { toA := { x := 1 }, y := 2 } : B

Lean understands what I mean by ({ x := 1, y := 2 } : B), and it also understands { x := 1, y := 2 : B }. But it always displays { toA := { x := 1 }, y := 2 } : B. I think it should delaborate this to { x := 1, y := 2 }. This is especially common in Mathlib which has deeply nested structures. Note that Lean 3 had the same behavior, but nested structures were a lot less common.

[Shreyas Srinivas]

Taking this even further, wouldn't it be convenient if it was in fact {x := 1, y := 2} rather than just delaborating to it? not only is it convenient, given let h := {x := 1, y := 2 : B} one might try to access h.x rather than h.toA.xand get errors.

[Patrick Massot]

No, you won't get an error.

[Patrick Massot]

You can simply try:

structure A :=
(x : nat)

structure B extends A :=
(y : nat)

def h := ({ x := 1, y := 2 } : B)

#check h.x

[Patrick Massot]

Direct access to a structure field is only the simplest use of dot notation in Lean.

[Shreyas Srinivas]

Thanks that helps

[Eric Wieser]

Shreyas Srinivas said:

Taking this even further, wouldn't it be convenient if it was in fact {x := 1, y := 2} rather than just delaborating to it?

Under the RFC at lean4#2666, this behavior can be recovered with

structure A where
  x : Nat

structure B extends @[flat] A where
  y : Nat

which means {x := 1, y := 2] is notation for .mk 1 2 as opposed to .mk (.mk 1) 2

[Eric Wieser]

(If you like that approach, I encourage you or anyone else reading to :+1: the RFC, as supposedly this has some impact on prioritization)