Merge remote-tracking branch 'upstream/nightly-testing' into lean4-pr…

…-3756

Std/Data/Array/Lemmas.lean

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Std.Data.List.Lemmas
-import Std.Data.Array.Init.Lemmas
 import Std.Data.Array.Basic
 import Std.Tactic.SeqFocus
 import Std.Util.ProofWanted

Std/Data/Array/Merge.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
+import Std.Tactic.Alias
 
 namespace Array
 

Std/Tactic/PrintPrefix.lean

@@ -73,12 +73,11 @@ private def lexNameLt : Name -> Name -> Bool
 | .str _ _, .num _ _ => false
 | .str p m, .str q n => m < n || m == n && lexNameLt p q
 
-private def appendMatchingConstants (msg : MessageData) (opts : PrintPrefixConfig) (pre : Name)
-     : MetaM MessageData := do
+private def matchingConstants (opts : PrintPrefixConfig) (pre : Name)
+     : MetaM (Array MessageData) := do
   let cinfos ← getMatchingConstants (matchName opts pre) opts.imported
   let cinfos := cinfos.qsort fun p q => lexNameLt (reverseName p.name) (reverseName q.name)
-  let mut msg := msg
-  let ppInfo cinfo : MetaM MessageData := do
+  cinfos.mapM fun cinfo => do
     if opts.showTypes then
       pure <| .ofPPFormat { pp := fun
         | some ctx => ctx.runMetaM <|
@@ -87,9 +86,6 @@ private def appendMatchingConstants (msg : MessageData) (opts : PrintPrefixConfi
       } ++ "\n"
     else
       pure m!"{ppConst (← mkConstWithLevelParams cinfo.name)}\n"
-  for cinfo in cinfos do
-    msg := msg ++ (← ppInfo cinfo)
-  pure msg
 
 /--
 The command `#print prefix foo` will print all definitions that start with
@@ -122,9 +118,8 @@ elab (name := printPrefix) "#print" tk:"prefix"
     cfg:(Lean.Parser.Tactic.config)? name:ident : command => liftTermElabM do
   let nameId := name.getId
   let opts ← elabPrintPrefixConfig (mkOptionalNode cfg)
-  let mut msg ← appendMatchingConstants "" opts nameId
-  if msg.isEmpty then
+  let mut msgs ← matchingConstants opts nameId
+  if msgs.isEmpty then
     if let [name] ← resolveGlobalConst name then
-      msg ← appendMatchingConstants msg opts name
-  if !msg.isEmpty then
-    logInfoAt tk msg
+      msgs ← matchingConstants opts name
+  logInfoAt tk (.joinSep msgs.toList "")

test/print_prefix.lean

@@ -12,6 +12,7 @@ TEmpty.recOn.{u} (motive : TEmpty → Sort u) (t : TEmpty) : motive t
 #guard_msgs in
 #print prefix TEmpty -- Test type that probably won't change much.
 
+/-- info: -/
 #guard_msgs in
 #print prefix (config := {imported := false}) Empty