Zulip Chat Archive

Stream: new members

Topic: Renaming fields of structures being extended


view this post on Zulip Kevin Sullivan (Mar 15 2021 at 19:23):

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?

view this post on Zulip Mario Carneiro (Mar 15 2021 at 19:49):

I've never heard of such a feature

view this post on Zulip Mario Carneiro (Mar 15 2021 at 19:50):

There is renaming in open IIRC but not in structure

view this post on Zulip Mario Carneiro (Mar 15 2021 at 19:50):

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

view this post on Zulip Mario Carneiro (Mar 15 2021 at 19:51):

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

view this post on Zulip Filippo A. E. Nuccio (Mar 15 2021 at 20:10):

@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:

view this post on Zulip Mario Carneiro (Mar 15 2021 at 20:24):

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 → ℕ

view this post on Zulip Eric Wieser (Mar 15 2021 at 20:57):

This feature does exist, the keyword is renaming

view this post on Zulip Filippo A. E. Nuccio (Mar 15 2021 at 22:30):

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.

view this post on Zulip Kevin Sullivan (Mar 16 2021 at 01:42):

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.

view this post on Zulip Julian Berman (Mar 16 2021 at 01:46):

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

view this post on Zulip Julian Berman (Mar 16 2021 at 01:46):

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


Last updated: May 16 2021 at 05:21 UTC