diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index ab2d244e3b..9a5516ca65 100644 --- 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 index a7c8f62c67..af1341aa19 100644 --- 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 index 07f82208a1..deee185b7a 100644 --- 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 index b867ef066d..778e9b8581 100644 --- 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 index 65a21b21fa..ef5233e044 100644 --- 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