{m : Type → Type} →
  [Monad m] →
    {α : Type} →
      (Lean.TraceData → Lean.MessageData → Array Lean.MessageData → m (Lean.MessageData.VisitStep✝ α)) →
        α → (α → α → α) → Lean.MessageData → m α