Zulip Chat Archive

Stream: new members

Topic: Rename structure projections


Nicolò Cavalleri (Jul 12 2021 at 09:53):

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

Eric Wieser (Jul 12 2021 at 11:08):

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 (Jul 12 2021 at 13:36):

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

Eric Wieser (Jul 12 2021 at 13:44):

Yes that's possible too

Eric Wieser (Jul 12 2021 at 13:44):

structure new_foo extends to_old_foo : foo I think

Nicolò Cavalleri (Jul 12 2021 at 14:52):

Ok great thanks!!


Last updated: Dec 20 2023 at 11:08 UTC