Name a structure in tactic mode

Stream: new members

[Igor Hańczaruk]

In my goal I have something like {big_structure_1}.trans {big_structure_2}. I want to do something like set p := {big_structure_1} with hp, but without writing whole {big_structure_1} explicitly. Alternatively I'd like to have whole structure displayed in goal info view, so I can copy it (by default some fields are replaced by '...').

[Mirek Olšák]

#new members > Way to use `set` without having to copy-paste expression?