Renaming fields of structures being extended

Stream: new members

[Kevin Sullivan]

Hi Folks,

I know that at one point Lean had an "extending x->y" construct enabling the renaming of field inherited from parent structures. So you could say, for example, "structure X extends Y renaming z->x." It appears (to me) that this feature has been changed or eliminated. Is there a way to rename fields of structures when extending structures?Also, it looks like the merging of multiply inherited field names is not happening. Is there up-to-date documentation on these aspects of Lean 3?

[Mario Carneiro]

I've never heard of such a feature

[Mario Carneiro]

There is renaming in open IIRC but not in structure

[Mario Carneiro]

Merging of multiply inherited field names happens when you set set_option old_structure_cmd true

[Mario Carneiro]

mathlib primarily uses the "old structure cmd" but lean 4 is doing away with it so we'll need to reimplement it in the mathlib prelude

[Filippo A. E. Nuccio]

@Mario Carneiro Since I was fighting with this problem a couple of days ago (trying to extend a structure, but Lean complaining that something with the same name already existed), can you point to some docsabout set_option old_structure_cmd true? Thanks! :pray:

[Mario Carneiro]

No particular docs to point to, but the usage is pretty simple:

set_option old_structure_cmd true
structure foo :=
(a : nat)
(b : nat)

structure bar :=
(a : nat)
(c : nat)

structure baz extends foo, bar

#print baz
-- structure baz : Type
-- fields:
-- baz.a : baz → ℕ
-- baz.b : baz → ℕ
-- baz.c : baz → ℕ

[Eric Wieser]

This feature does exist, the keyword is renaming

[Filippo A. E. Nuccio]

Mario Carneiro said:

No particular docs to point to, but the usage is pretty simple:

set_option old_structure_cmd true
structure foo :=
(a : nat)
(b : nat)

structure bar :=
(a : nat)
(c : nat)

structure baz extends foo, bar

#print baz
-- structure baz : Type
-- fields:
-- baz.a : baz → ℕ
-- baz.b : baz → ℕ
-- baz.c : baz → ℕ

Thanks! No docs beats such an example.

[Kevin Sullivan]

Eric Wieser said:

This feature does exist, the keyword is renaming

I get syntax errors at "renaming" when I copy and paste old code that presumably used to work.

[Julian Berman]

https://github.com/leanprover-community/lean/blob/cab92ef9f05754271116ab6786890d558c53e746/tests/lean/run/record10.lean#L7-L8

[Julian Berman]

In case that helps, grepping the test suite finds some examples that presumably still work/run in CI?