Lean4
/-- Returns the projection information of a structure. -/
def projectionsInfo (l : List ProjectionData) (pref : String) (str : Name) : MessageData :=
let ⟨defaults, nondefaults⟩ := l.partition (·.isDefault)
let toPrint : List MessageData :=
defaults.map fun s ↦
let prefixStr := if s.isPrefix then "(prefix) " else ""
m! "Projection {prefixStr }{s.name }: {s.expr}"
let print2 : MessageData := String.join <| (nondefaults.map fun nm : ProjectionData ↦ toString nm.1).intersperse ", "
let toPrint :=
toPrint ++
if nondefaults.isEmpty then []
else [("No lemmas are generated for the projections: " : MessageData) ++ print2 ++ "."]
let toPrint := MessageData.joinSep toPrint ("\n" : MessageData)
m! "{pref } {str }:\n{toPrint}"
