Rename structure projections

Stream: new members

[Nicolò Cavalleri]

What is the simplest way to rename the automatic projections of a structure that extends another structure?

[Eric Wieser]

Are you looking for something like this?

-- only works with `old_structure_cmd`
set_option old_structure_cmd true

structure foo := (bar : nat)

structure new_foo extends foo renaming bar → baz

[Nicolò Cavalleri]

Actually I am looking to rename what in your example is to_foo, sorry for not being precise!

[Eric Wieser]

Yes that's possible too

[Eric Wieser]

structure new_foo extends to_old_foo : foo I think

[Nicolò Cavalleri]

Ok great thanks!!