expand all members within a type class

Stream: lean4

[lexuan]

In Lean 4, is there a way to view all the fields contained in a type class, including all the fields defined by it and all the fields of the inheriting classes (this means, all fields including the fields of inheritances of inheritances)? If there is no ready-made statement that can achieve this, how then should one write a program to achieve this functionality? GitHub Copilot has not been able to solve this difficulty, using a lot of erroneous code.

[Floris van Doorn]

If it's in Mathlib/Batteries/Core, then you can just look at the generated docs, e.g. docs#Field

[lexuan]

Thank you for sharing, this method is very helpful. However, how should I proceed if I want to implement this in VSCode? Is there a syntax similar to #check?

[Floris van Doorn]

You should be able to get this with metaprogramming quite quickly, probably by looking at the doc-gen code that generates this list.

[lexuan]

Understood, thank you for the answer.