Zulip Chat Archive

Stream: lean4

Topic: improving #print structure


Eric Wieser (Feb 19 2024 at 11:03):

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 (Feb 19 2024 at 11:04):

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

Eric Wieser (Feb 19 2024 at 11:06):

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 (Mar 26 2024 at 23:30):

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!


Last updated: May 02 2025 at 03:31 UTC