Recursive `where` for structure instances?

Stream: lean4

[Thomas Murrills]

In Lean.Elab.StructInst, I noticed the following in the module docstring that explains what form structure instances can take:

/-!
...
def structInstWhereBody := leading_parser
  structInstFields (sepByIndent structInstField "; " (allowTrailingSep := true))

@[builtin_structInstFieldDecl_parser]
def structInstFieldWhere := leading_parser
  "where" >> structInstWhereBody
-/

As far as I can tell, these don't exist (even under another name). Are they outdated, or aspirational? :)

[Jakub Nowak]

The commit message from the blame does say

The PR also is setting things up for future expansion. Pending some
discussion, in the future structure/where notation could have have
embedded where clauses; rather than { a := { x := 1, y := z } } one
could write { a where x := 1; y := z }.

https://github.com/leanprover/lean4/commit/a1c3a36433f74257a2a332b3e0b2a6f6631a9713

Btw, the syntax for recursive nested structures is:

structure Foo where
  n : Nat

structure Bar where
  foo : Foo

def bar : Bar where
  foo.n := 2

[Thomas Murrills]

Ah, I looked through the issues and zulip, but forgot to check the blame. Nice! :)

[Jakub Nowak]

Actually, exactly the same commit introduced the recursive syntax I mentioned, so I guess where was considered but never implemented in the end.

[Thomas Murrills]

Hmm, that sounds a bit unusual...perhaps the thought is that we might still want to allow where eventually, but foo.n-style recursive syntax is at least functional in the meantime?

[Thomas Murrills]

I suppose we might want to simply ping @Kyle Miller to shed some light on this question. :grinning_face_with_smiling_eyes:

[Jakub Nowak]

Yeah, I've tried searching for this past discussion but couldn't find it.