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