Commit 2023-06-07 08:52 f06b52fa

feat: add commutative diagram widget (#3583) Adds a widget for displaying goals in the language of category theory as commutative diagrams. Examples are found in test/CommDiag.lean. The set of diagram shapes which can be visualized is extensible via the @[expr_presenter] attribute. The widget is triggered in a tactic proof using the with_panel_widgets [GoalTypePanel] tactic combinator. Support for globally enabling the widget in a given file is planned for another PR. Continued from #363, please see there for more discussion.