improving #print structure

Stream: lean4

[Eric Wieser]

If I want to know the definition of a structure from the editor, my default is to try #print.
Unfortunately, this gives me nothing useful:

#print Lean.Meta.Simp.Config
inductive Lean.Meta.Simp.Config : Type
number of parameters: 0
constructors:
Lean.Meta.Simp.Config.mk : ℕ →
  ℕ →
    Bool →
      Bool →
        Bool →
          Bool →
            Bool →
              Bool →
                Meta.EtaStructMode → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Meta.Simp.Config

Could this be changed to at least show the parameter names?

[Joachim Breitner]

And while we are at it, maybe don’t indent after → (it doesn’t indent the various parameters when printing them using ∀)?

[Eric Wieser]

By contrast, in Lean 3, #print prod gives

@[derive list.cons.{0} pexpr ``(has_reflect) (list.nil.{0} pexpr)]
structure prod : Type u → Type v → Type (max u v)
fields:
prod.fst : Π {α : Type u} {β : Type v}, α × β → α
prod.snd : Π {α : Type u} {β : Type v}, α × β → β

which is much more useful

[François G. Dorais]

Sorry to revive an old thread. There is now an RFC to fix this issue at lean4#3644 as well as a WIP PR to implement it at lean4#3768. Please thumbs up the issue if you think this is useful!