feat: have #print show precise fields of structures (#6096)

This PR improves the `#print` command for structures to show all fields
and which parents the fields were inherited from, hiding internal
details such as which parents are represented as subobjects. This
information is still present in the constructor if needed. The pretty
printer for private constants is also improved, and it now handles
private names from the current module like any other name; private names
from other modules are made hygienic.

Example output for `#print Monad`:
```
class Monad.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
number of parameters: 1
parents:
  Monad.toApplicative : Applicative m
  Monad.toBind : Bind m
fields:
  Functor.map : {α β : Type u} → (α → β) → m α → m β
  Functor.mapConst : {α β : Type u} → α → m β → m α
  Pure.pure : {α : Type u} → α → m α
  Seq.seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β
  SeqLeft.seqLeft : {α β : Type u} → m α → (Unit → m β) → m α
  SeqRight.seqRight : {α β : Type u} → m α → (Unit → m β) → m β
  Bind.bind : {α β : Type u} → m α → (α → m β) → m β
constructor:
  Monad.mk.{u, v} {m : Type u → Type v} [toApplicative : Applicative m] [toBind : Bind m] : Monad m
resolution order:
  Monad, Applicative, Bind, Functor, Pure, Seq, SeqLeft, SeqRight
```

Suggested by Floris van Doorn [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.23print.20command.20for.20structures/near/482503637).

src/Lean/Elab/Print.lean

@@ -22,7 +22,7 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
       m := m ++ ", " ++ toMessageData u
     return m ++ "}"
 
-private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
+private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do
   let m : MessageData :=
     match (← getReducibilityStatus id) with
     | ReducibilityStatus.irreducible => "@[irreducible] "
@@ -38,11 +38,13 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   let (m, id) := match privateToUserName? id with
     | some id => (m ++ "private ", id)
     | none    => (m, id)
-  let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type
-  pure m
+  if sig then
+    return m!"{m}{kind} {id}{levelParamsToMessageData levelParams} : {type}"
+  else
+    return m!"{m}{kind}"
 
-private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData :=
-  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe)
+private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) (sig : Bool := true) : CommandElabM MessageData :=
+  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) (sig := sig)
 
 private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
   let m ← mkHeader kind id levelParams type safety
@@ -65,32 +67,63 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
   logInfo m
 
+/--
+Computes the origin of a field. Returns its projection function at the origin.
+Multiple parents could be the origin of a field, but we say the first parent that provides it is the one that determines the origin.
+-/
+private partial def getFieldOrigin (structName field : Name) : MetaM Name := do
+  let env ← getEnv
+  for parent in getStructureParentInfo env structName do
+    if (findField? env parent.structName field).isSome then
+      return ← getFieldOrigin parent.structName field
+  let some fi := getFieldInfo? env structName field
+    | throwError "no such field {field} in {structName}"
+  return fi.projFn
+
 open Meta in
 private def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
-    (ctor : Name) (fields : Array Name) (isUnsafe : Bool) (isClass : Bool) : CommandElabM Unit := do
-  let kind := if isClass then "class" else "structure"
-  let mut m ← mkHeader' kind id levelParams type isUnsafe
-  m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
-  m := m ++ Format.line ++ "constructor:"
-  let cinfo ← getConstInfo ctor
-  m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
-  m := m ++ Format.line ++ "fields:" ++ (← doFields)
-  logInfo m
-where
-  doFields := liftTermElabM do
-    forallTelescope (← getConstInfo id).type fun params _ =>
-      withLocalDeclD `self (mkAppN (Expr.const id (levelParams.map .param)) params) fun self => do
-        let params := params.push self
-        let mut m : MessageData := ""
+    (isUnsafe : Bool) : CommandElabM Unit := do
+  let env ← getEnv
+  let kind := if isClass env id then "class" else "structure"
+  let header ← mkHeader' kind id levelParams type isUnsafe (sig := false)
+  liftTermElabM <| forallTelescope (← getConstInfo id).type fun params _ =>
+    let s := Expr.const id (levelParams.map .param)
+    withLocalDeclD `self (mkAppN s params) fun self => do
+      let mut m : MessageData := header
+      -- Signature
+      m := m ++ " " ++ .ofFormatWithInfosM do
+        let (stx, infos) ← PrettyPrinter.delabCore s (delab := PrettyPrinter.Delaborator.delabConstWithSignature)
+        pure ⟨← PrettyPrinter.ppTerm ⟨stx⟩, infos⟩
+      m := m ++ Format.line ++ m!"number of parameters: {numParams}"
+      -- Parents
+      let parents := getStructureParentInfo env id
+      unless parents.isEmpty do
+        m := m ++ Format.line ++ "parents:"
+        for parent in parents do
+          let ptype ← inferType (mkApp (mkAppN (.const parent.projFn (levelParams.map .param)) params) self)
+          m := m ++ indentD m!"{.ofConstName parent.projFn (fullNames := true)} : {ptype}"
+      -- Fields
+      let fields := getStructureFieldsFlattened env id (includeSubobjectFields := false)
+      if fields.isEmpty then
+        m := m ++ Format.line ++ "fields: (none)"
+      else
+        m := m ++ Format.line ++ "fields:"
         for field in fields do
-          match getProjFnForField? (← getEnv) id field with
-          | some proj =>
-            let field : Format := if isPrivateName proj then "private " ++ toString field else toString field
-            let cinfo ← getConstInfo proj
-            let ftype ← instantiateForall cinfo.type params
-            m := m ++ Format.line ++ field ++ " : " ++ ftype
-          | none => panic! "missing structure field info"
-        addMessageContext m
+          let some source := findField? env id field | panic! "missing structure field info"
+          let proj ← getFieldOrigin source field
+          let modifier := if isPrivateName proj then "private " else ""
+          let ftype ← inferType (← mkProjection self field)
+          m := m ++ indentD (m!"{modifier}{.ofConstName proj (fullNames := true)} : {ftype}")
+      -- Constructor
+      let cinfo := getStructureCtor (← getEnv) id
+      let ctorModifier := if isPrivateName cinfo.name then "private " else ""
+      m := m ++ Format.line ++ "constructor:" ++ indentD (ctorModifier ++ .signature cinfo.name)
+      -- Resolution order
+      let resOrder ← getStructureResolutionOrder id
+      if resOrder.size > 1 then
+        m := m ++ Format.line ++ "resolution order:"
+          ++ indentD (MessageData.joinSep (resOrder.map (.ofConstName · (fullNames := true))).toList ", ")
+      logInfo m
 
 private def printIdCore (id : Name) : CommandElabM Unit := do
   let env ← getEnv
@@ -103,11 +136,10 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
   | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
-    match getStructureInfo? env id with
-    | some { fieldNames, .. } =>
-      let [ctor] := ctors | panic! "structures have only one constructor"
-      printStructure id us numParams t ctor fieldNames u (isClass env id)
-    | none => printInduct id us numParams t ctors u
+    if isStructure env id then
+      printStructure id us numParams t u
+    else
+      printInduct id us numParams t ctors u
   | none => throwUnknownId id
 
 private def printId (id : Syntax) : CommandElabM Unit := do

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -91,21 +91,32 @@ Rather, it is called through the `app` delaborator.
 -/
 def delabConst : Delab := do
   let Expr.const c₀ ls ← getExpr | unreachable!
-  let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀
-
-  let mut c ← unresolveNameGlobal c₀ (fullNames := ← getPPOption getPPFullNames)
-  let stx ← if ls.isEmpty || !(← getPPOption getPPUniverses) then
-    if (← getLCtx).usesUserName c then
-      -- `c` is also a local declaration
-      if c == c₀ && !(← read).inPattern then
-        -- `c` is the fully qualified named. So, we append the `_root_` prefix
-        c := `_root_ ++ c
+  let mut c₀ := c₀
+  let mut c  := c₀
+  if let some n := privateToUserName? c₀ then
+    unless (← getPPOption getPPPrivateNames) do
+      if c₀ == mkPrivateName (← getEnv) n then
+        -- The name is defined in this module, so use `n` as the name and unresolve like any other name.
+        c₀ := n
+        c ← unresolveNameGlobal n (fullNames := ← getPPOption getPPFullNames)
       else
-        c := c₀
-    pure <| mkIdent c
+        -- The name is not defined in this module, so make inaccessible. Unresolving does not make sense to do.
+        c ← withFreshMacroScope <| MonadQuotation.addMacroScope n
   else
-    let mvars ← getPPOption getPPMVarsLevels
-    `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
+    c ← unresolveNameGlobal c (fullNames := ← getPPOption getPPFullNames)
+  let stx ←
+    if ls.isEmpty || !(← getPPOption getPPUniverses) then
+      if (← getLCtx).usesUserName c then
+        -- `c` is also a local declaration
+        if c == c₀ && !(← read).inPattern then
+          -- `c` is the fully qualified named. So, we append the `_root_` prefix
+          c := `_root_ ++ c
+        else
+          c := c₀
+      pure <| mkIdent c
+    else
+      let mvars ← getPPOption getPPMVarsLevels
+      `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
 
   let stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then

tests/lean/diamond1.lean.expected.out

@@ -2,14 +2,20 @@ diamond1.lean:11:40-11:45: error: parent field type mismatch, field 'a' from par
   α → α : Type
 but is expected to have type
   α : Type
-structure Foo : Type → Type
+structure Foo (α : Type) : Type
 number of parameters: 1
-constructor:
-Foo.mk : {α : Type} → Bar (α → α) → (Bool → α) → Nat → Foo α
+parents:
+  Foo.toBar : Bar (α → α)
+  Foo.toBaz : Baz α
 fields:
-toBar : Bar (α → α)
-c : Bool → α
-d : Nat
+  Bar.a : α → α
+  Bar.b : Nat → α → α
+  Baz.c : Bool → α
+  Baz.d : Nat
+constructor:
+  Foo.mk {α : Type} (toBar : Bar (α → α)) (c : Bool → α) (d : Nat) : Foo α
+resolution order:
+  Foo, Bar, Baz
 def f : Nat → Foo Nat :=
 fun x => { a := fun y => x + y, b := fun x1 x2 => x1 + x2, c := fun x_1 => x, d := x }
 diamond1.lean:27:47-27:52: warning: field 'a' from 'Baz' has already been declared

tests/lean/diamond8.lean.expected.out

@@ -1,7 +1,16 @@
-class Semiring.{u} : Type u → Type u
+class Semiring.{u} (R : Type u) : Type u
 number of parameters: 1
-constructor:
-Semiring.mk : {R : Type u} → [toAddCommMonoid : AddCommMonoid R] → [toMonoid : Monoid R] → Semiring R
+parents:
+  Semiring.toAddCommMonoid : AddCommMonoid R
+  Semiring.toMonoidWithZero : MonoidWithZero R
+  Semiring.toOne : One R
 fields:
-toAddCommMonoid : AddCommMonoid R
-toMonoid : Monoid R
+  Add.add : R → R → R
+  Zero.zero : R
+  Mul.mul : R → R → R
+  One.one : R
+  Monoid.mul_one : ∀ (m : R), m * 1 = m
+constructor:
+  Semiring.mk.{u} {R : Type u} [toAddCommMonoid : AddCommMonoid R] [toMonoid : Monoid R] : Semiring R
+resolution order:
+  Semiring, AddCommMonoid, MonoidWithZero, Add, Monoid, Zero, Mul, One

tests/lean/printStructure.lean

@@ -1,94 +1,152 @@
 /-!
-  Test #print command for structures and classes
+# Test `#print` command for structures and classes
 -/
 
-/- Structure -/
+/-! Structure -/
 /--
-info: structure Prod.{u, v} : Type u → Type v → Type (max u v)
+info: structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
 number of parameters: 2
-constructor:
-Prod.mk : {α : Type u} → {β : Type v} → α → β → α × β
 fields:
-fst : α
-snd : β
+  Prod.fst : α
+  Prod.snd : β
+constructor:
+  Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β
 -/
 #guard_msgs in
 #print Prod
 
-/- Class -/
+/-! Class -/
 /--
-info: class Inhabited.{u} : Sort u → Sort (max 1 u)
+info: class Inhabited.{u} (α : Sort u) : Sort (max 1 u)
 number of parameters: 1
-constructor:
-Inhabited.mk : {α : Sort u} → α → Inhabited α
 fields:
-default : α
+  Inhabited.default : α
+constructor:
+  Inhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α
 -/
 #guard_msgs in
 #print Inhabited
 
-/- Structure with private field -/
+/-! Structure with private field, imported -/
 /--
-info: structure Thunk.{u} : Type u → Type u
+info: structure Thunk.{u} (α : Type u) : Type u
 number of parameters: 1
-constructor:
-Thunk.mk : {α : Type u} → (Unit → α) → Thunk α
 fields:
-private fn : Unit → α
+  private Thunk.fn✝ : Unit → α
+constructor:
+  Thunk.mk.{u} {α : Type u} (fn : Unit → α) : Thunk α
 -/
 #guard_msgs in
 #print Thunk
 
-/- Extended class -/
+/-! Structure with private field, current module -/
+structure PrivField where
+  private x : Nat
+
 /--
-info: class Alternative.{u, v} : (Type u → Type v) → Type (max (u + 1) v)
-number of parameters: 1
-constructor:
-Alternative.mk : {f : Type u → Type v} →
-  [toApplicative : Applicative f] → ({α : Type u} → f α) → ({α : Type u} → f α → (Unit → f α) → f α) → Alternative f
+info: structure PrivField : Type
+number of parameters: 0
 fields:
-toApplicative : Applicative f
-failure : {α : Type u} → f α
-orElse : {α : Type u} → f α → (Unit → f α) → f α
+  private PrivField.x : Nat
+constructor:
+  PrivField.mk (x : Nat) : PrivField
+-/
+#guard_msgs in
+#print PrivField
+
+/-! Private constructor, imported -/
+/--
+info: class TypeName.{u} (α : Type u) : Type
+number of parameters: 1
+fields:
+  private TypeName.data✝ : (TypeNameData✝ α).type
+constructor:
+  private TypeName.mk'✝.{u} {α : Type u} (data : (TypeNameData✝ α).type) : TypeName α
+-/
+#guard_msgs in
+#print TypeName
+
+/-! Private constructor, current module -/
+structure PrivCtor where private mk ::
+  x : Nat
+/--
+info: structure PrivCtor : Type
+number of parameters: 0
+fields:
+  PrivCtor.x : Nat
+constructor:
+  private PrivCtor.mk (x : Nat) : PrivCtor
+-/
+#guard_msgs in
+#print PrivCtor
+
+/-! Extended class -/
+/--
+info: class Alternative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
+number of parameters: 1
+parents:
+  Alternative.toApplicative : Applicative f
+fields:
+  Functor.map : {α β : Type u} → (α → β) → f α → f β
+  Functor.mapConst : {α β : Type u} → α → f β → f α
+  Pure.pure : {α : Type u} → α → f α
+  Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
+  SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
+  SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β
+  Alternative.failure : {α : Type u} → f α
+  Alternative.orElse : {α : Type u} → f α → (Unit → f α) → f α
+constructor:
+  Alternative.mk.{u, v} {f : Type u → Type v} [toApplicative : Applicative f] (failure : {α : Type u} → f α)
+    (orElse : {α : Type u} → f α → (Unit → f α) → f α) : Alternative f
+resolution order:
+  Alternative, Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
 -/
 #guard_msgs in
 #print Alternative
 
-/- Multiply extended class -/
+/-! Multiply extended class -/
 /--
-info: class Applicative.{u, v} : (Type u → Type v) → Type (max (u + 1) v)
+info: class Applicative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
 number of parameters: 1
-constructor:
-Applicative.mk : {f : Type u → Type v} →
-  [toFunctor : Functor f] →
-    [toPure : Pure f] → [toSeq : Seq f] → [toSeqLeft : SeqLeft f] → [toSeqRight : SeqRight f] → Applicative f
+parents:
+  Applicative.toFunctor : Functor f
+  Applicative.toPure : Pure f
+  Applicative.toSeq : Seq f
+  Applicative.toSeqLeft : SeqLeft f
+  Applicative.toSeqRight : SeqRight f
 fields:
-toFunctor : Functor f
-toPure : Pure f
-toSeq : Seq f
-toSeqLeft : SeqLeft f
-toSeqRight : SeqRight f
+  Functor.map : {α β : Type u} → (α → β) → f α → f β
+  Functor.mapConst : {α β : Type u} → α → f β → f α
+  Pure.pure : {α : Type u} → α → f α
+  Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
+  SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
+  SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β
+constructor:
+  Applicative.mk.{u, v} {f : Type u → Type v} [toFunctor : Functor f] [toPure : Pure f] [toSeq : Seq f]
+    [toSeqLeft : SeqLeft f] [toSeqRight : SeqRight f] : Applicative f
+resolution order:
+  Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
 -/
 #guard_msgs in
 #print Applicative
 
-/- Structure with unused parameter -/
+/-! Structure with unused parameter -/
 
 structure Weird (α β : Type _) where
   a : α
 
 /--
-info: structure Weird.{u_1, u_2} : Type u_1 → Type u_2 → Type u_1
+info: structure Weird.{u_1, u_2} (α : Type u_1) (β : Type u_2) : Type u_1
 number of parameters: 2
-constructor:
-Weird.mk : {α : Type u_1} → {β : Type u_2} → α → Weird α β
 fields:
-a : α
+  Weird.a : α
+constructor:
+  Weird.mk.{u_1, u_2} {α : Type u_1} {β : Type u_2} (a : α) : Weird α β
 -/
 #guard_msgs in
 #print Weird
 
-/- Structure-like inductive -/
+/-! Structure-like inductive -/
 
 inductive Fake (α : Type _) where
   | mk : (x : α) → Fake α

tests/lean/run/2291.lean

@@ -21,13 +21,13 @@ let _x_29 := Lean.Expr.const _x_28 _x_25;
 let _x_30 := _x_29.app _x_23;
 let _x_31 := [];
 let _x_32 := 0 :: _x_31;
-let _x_33 := Lean.List.toExprAux _x_27 _x_30 _x_32;
+let _x_33 := Lean.List.toExprAux✝ _x_27 _x_30 _x_32;
 Lean.MessageData.ofExpr _x_33
 [compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
 fun nilFn consFn x =>
   List.casesOn fun head tail =>
     let _x_1 := Lean.mkNatLit head;
-    let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail;
+    let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail;
     Lean.mkAppB consFn _x_1 _x_2
 >> _eval
 let _x_14 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
@@ -41,13 +41,13 @@ let _x_21 := `List.cons;
 let _x_22 := Lean.Expr.const._override _x_21 _x_18;
 let _x_23 := Lean.Expr.app._override _x_22 _x_16;
 let _x_24 := List.cons _neutral 0 _x_15;
-let _x_25 := Lean.List.toExprAux._at._eval._spec_1 _x_20 _x_23 _x_24;
+let _x_25 := Lean.List.toExprAux._at._eval._spec_1✝ _x_20 _x_23 _x_24;
 Lean.MessageData.ofExpr _x_25
 [compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
 fun nilFn consFn x =>
   List.casesOn fun head tail =>
     let _x_1 := Lean.mkNatLit head;
-    let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail;
+    let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail;
     Lean.mkAppB consFn _x_1 _x_2
 >> _eval
 let _x_1 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
@@ -61,13 +61,13 @@ let _x_8 := `List.cons;
 let _x_9 := Lean.Expr.const._override _x_8 _x_5;
 let _x_10 := Lean.Expr.app._override _x_9 _x_3;
 let _x_11 := List.cons _neutral 0 _x_2;
-let _x_12 := Lean.List.toExprAux._at._eval._spec_1 _x_7 _x_10 _x_11;
+let _x_12 := Lean.List.toExprAux._at._eval._spec_1✝ _x_7 _x_10 _x_11;
 Lean.MessageData.ofExpr _x_12
 [compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
 fun nilFn consFn x =>
   List.casesOn fun head tail =>
     let _x_1 := Lean.mkNatLit head;
-    let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail;
+    let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail;
     Lean.mkAppB consFn _x_1 _x_2
 >> _eval._closed_1
 "Nat"
@@ -102,7 +102,7 @@ let _x_1 := List.nil _neutral;
 List.cons _neutral 0 _x_1
 >> _eval
 let _x_1 :=
-  Lean.List.toExprAux._at._eval._spec_1 _eval._closed_9 _eval._closed_13
+  Lean.List.toExprAux._at._eval._spec_1✝ _eval._closed_9 _eval._closed_13
     _eval._closed_14;
 Lean.MessageData.ofExpr _x_1
 ---

tests/lean/run/4465.lean

@@ -3,7 +3,7 @@
 #reduce Char.ofNat (nat_lit 0)
 
 /--
-info: { val := { toBitVec := { toFin := ⟨0, isValidChar_UInt32 (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ } },
+info: { val := { toBitVec := { toFin := ⟨0, isValidChar_UInt32✝ (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ } },
   valid := Or.inl (Nat.le_of_ble_eq_true rfl) }
 -/
 #guard_msgs in

tests/lean/run/print_cmd.lean

@@ -2,18 +2,99 @@
 
 private def foo (x : Nat) : Nat := x + 1
 
-#print "hello"
-#print id
-#print propext
-#print default
-#print ReaderT.read
-#print Prod
-#print Prod.mk
-#print Nat
-#print Nat.succ
-#print Nat.rec
-#print Nat.casesOn
-#print foo
-#print Quot.mk
-#print Quot.ind
-#print Quot.mk
+/-- info: hello -/
+#guard_msgs in #print "hello"
+/--
+info: def id.{u} : {α : Sort u} → α → α :=
+fun {α} a => a
+-/
+#guard_msgs in #print id
+/-- info: axiom propext : ∀ {a b : Prop}, (a ↔ b) → a = b -/
+#guard_msgs in #print propext
+/--
+info: def Inhabited.default.{u} : {α : Sort u} → [self : Inhabited α] → α :=
+fun α [self : Inhabited α] => self.1
+-/
+#guard_msgs in #print default
+/--
+info: protected def ReaderT.read.{u, v} : {ρ : Type u} → {m : Type u → Type v} → [inst : Monad m] → ReaderT ρ m ρ :=
+fun {ρ} {m} [Monad m] => pure
+-/
+#guard_msgs in #print ReaderT.read
+/--
+info: structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
+number of parameters: 2
+fields:
+  Prod.fst : α
+  Prod.snd : β
+constructor:
+  Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β
+-/
+#guard_msgs in #print Prod
+/-- info: constructor Prod.mk.{u, v} : {α : Type u} → {β : Type v} → α → β → α × β -/
+#guard_msgs in #print Prod.mk
+/--
+info: inductive Nat : Type
+number of parameters: 0
+constructors:
+Nat.zero : Nat
+Nat.succ : Nat → Nat
+-/
+#guard_msgs in #print Nat
+/-- info: constructor Nat.succ : Nat → Nat -/
+#guard_msgs in #print Nat.succ
+/--
+info: recursor Nat.rec.{u} : {motive : Nat → Sort u} →
+  motive Nat.zero → ((n : Nat) → motive n → motive n.succ) → (t : Nat) → motive t
+-/
+#guard_msgs in #print Nat.rec
+/--
+info: @[reducible] def Nat.casesOn.{u} : {motive : Nat → Sort u} →
+  (t : Nat) → motive Nat.zero → ((n : Nat) → motive n.succ) → motive t :=
+fun {motive} t zero succ => Nat.rec zero (fun n n_ih => succ n) t
+-/
+#guard_msgs in #print Nat.casesOn
+/--
+info: private def foo : Nat → Nat :=
+fun x => x + 1
+-/
+#guard_msgs in #print foo
+/-- info: Quotient primitive Quot.mk.{u} : {α : Sort u} → (r : α → α → Prop) → α → Quot r -/
+#guard_msgs in #print Quot.mk
+/--
+info: Quotient primitive Quot.ind.{u} : ∀ {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop},
+  (∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q
+-/
+#guard_msgs in #print Quot.ind
+/-- info: Quotient primitive Quot.mk.{u} : {α : Sort u} → (r : α → α → Prop) → α → Quot r -/
+#guard_msgs in #print Quot.mk
+
+/-!
+Structure with diamond inheritance
+-/
+structure A where
+  a : Nat
+structure B extends A where
+  b : Nat
+structure C extends A where
+  c : Nat
+structure D extends B, C where
+  d : Nat
+
+/--
+info: structure D : Type
+number of parameters: 0
+parents:
+  D.toB : B
+  D.toC : C
+fields:
+  A.a : Nat
+  B.b : Nat
+  C.c : Nat
+  D.d : Nat
+constructor:
+  D.mk (toB : B) (c d : Nat) : D
+resolution order:
+  D, B, C, A
+-/
+#guard_msgs in #print D

tests/lean/structAutoBound.lean.expected.out

@@ -1,16 +1,16 @@
-structure Foo.{v, u_1} : {α : Sort u_1} → (α → Type v) → Sort (max u_1 (v + 1))
+structure Foo.{v, u_1} {α : Sort u_1} (β : α → Type v) : Sort (max u_1 (v + 1))
 number of parameters: 2
-constructor:
-Foo.mk : {α : Sort u_1} → {β : α → Type v} → (a : α) → β a → Foo β
 fields:
-a : α
-b : β self.a
+  Foo.a : α
+  Foo.b : β self.a
+constructor:
+  Foo.mk.{v, u_1} {α : Sort u_1} {β : α → Type v} (a : α) (b : β a) : Foo β
 structAutoBound.lean:9:15-9:16: error: a universe level named 'u' has already been declared
-structure Boo.{u, v} : Type u → Type v → Type (max u v)
+structure Boo.{u, v} (α : Type u) (β : Type v) : Type (max u v)
 number of parameters: 2
-constructor:
-Boo.mk : {α : Type u} → {β : Type v} → α → β → Boo α β
 fields:
-a : α
-b : β
+  Boo.a : α
+  Boo.b : β
+constructor:
+  Boo.mk.{u, v} {α : Type u} {β : Type v} (a : α) (b : β) : Boo α β
 structAutoBound.lean:18:10-18:44: error: unused universe parameter 'w'