Extra utilities for Lean.MessageData

def ImportGraph.Lean.MessageData.bulletList (msgs : List Lean.MessageData) (forceList : Bool := true) : Lean.MessageData

Given [msg₁, msg₂, ...], creates a bulleted list of the form

• msg₁
• msg₂
...

By default, a single-message list [msg] is still rendered as • msg. If instead forceList := false, then a single-message list [msg] is rendered simply as msg.

Equations

• One or more equations did not get rendered due to their size.