structure extensions

Stream: lean4

[Anthony Bordg]

Is there a convenient way to search for all the extensions (lean keyword extends) of a given structure, e.g. Equiv?

[Kyle Miller]

I don't believe so, but the data is available

[Kyle Miller]

docs#Lean.structureExt via docs#Lean.StructureInfo.parentInfo

You'd have to iterate through all structures and see what's in the parentInfo fields to see what extends a given structure

[Kyle Miller]

I wonder if docgen should show this information, like how it shows instances already. (By the way: if you are ever wondering about class in particular, then these all appear in the instances list on docgen)

[Anthony Bordg]

Kyle Miller said:

I wonder if docgen should show this information

It could be useful.