metaprogramming and structure inheritance

Stream: general

[Simon Hudon]

I'm trying to write a tactic that explores the inheritance structure. Given the name of a structure type, can I discover what are its ancestors?

[Sebastian Ullrich]

Only for the new structure command. You need to reimplement get_parent_structures, but that shouldn't be too hard.

[Sebastian Ullrich]

tl;dr: subobject fields start with "_"

[Simon Hudon]

How does one use the new structure command? Also, is get_parent_structures exposed to Lean?

[Andrew Ashworth]

you're using the new structure command by default, I think

[Andrew Ashworth]

as opposed to the old structure command which is accessed with set option

[Sebastian Ullrich]

yep

[Simon Hudon]

Thanks! And is it possible that structure_fields by default does not list those symbols starting with _?

[Sebastian Ullrich]

Sorry, that was ambiguous. It's only in the inductive constructor parameters that they are encoded with _

[Sebastian Ullrich]

All structure_fields does is get the parameter names and strip any leading _

[Simon Hudon]

Let's say that I'm constructing an instance of group (but I don't know in the tactic that it is specifically group). I'd like to know that monoid is a direct parent so that I can use mk_instance and use the result as a source in pexpr.mk_structure_instance. How would you do it?