chore: in #print for structures, mention 'field notation' (#6406)

This PR modifies `#print` for structures to say "field notation resolution order" instead of just "resolution order".
leanprover · Dec 17, 2024 · 64d3e9a · 64d3e9a
1 parent 1880c61
commit 64d3e9a
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 6 deletions.
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
@@ -121,7 +121,7 @@ private def printStructure (id : Name) (levelParams : List Name) (numParams : Na
       -- Resolution order
       let resOrder ← getStructureResolutionOrder id
       if resOrder.size > 1 then
-        m := m ++ Format.line ++ "resolution order:"
+        m := m ++ Format.line ++ "field notation resolution order:"
           ++ indentD (MessageData.joinSep (resOrder.map (.ofConstName · (fullNames := true))).toList ", ")
       logInfo m
 

diff --git a/tests/lean/diamond1.lean.expected.out b/tests/lean/diamond1.lean.expected.out
@@ -14,7 +14,7 @@ fields:
   Baz.d : Nat
 constructor:
   Foo.mk {α : Type} (toBar : Bar (α → α)) (c : Bool → α) (d : Nat) : Foo α
-resolution order:
+field notation 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 }

diff --git a/tests/lean/diamond8.lean.expected.out b/tests/lean/diamond8.lean.expected.out
@@ -12,5 +12,5 @@ fields:
   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:
+field notation resolution order:
   Semiring, AddCommMonoid, MonoidWithZero, Add, Monoid, Zero, Mul, One
diff --git a/tests/lean/printStructure.lean b/tests/lean/printStructure.lean
@@ -98,7 +98,7 @@ fields:
 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:
+field notation resolution order:
   Alternative, Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
 -/
 #guard_msgs in
@@ -124,7 +124,7 @@ fields:
 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:
+field notation resolution order:
   Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
 -/
 #guard_msgs in

diff --git a/tests/lean/run/print_cmd.lean b/tests/lean/run/print_cmd.lean
@@ -94,7 +94,7 @@ fields:
   D.d : Nat
 constructor:
   D.mk (toB : B) (c d : Nat) : D
-resolution order:
+field notation resolution order:
   D, B, C, A
 -/
 #guard_msgs in #print D