Commit 2025-04-13 17:25 b796a62f
View on Github →fix: remove notation hacks in monoidal categories (#24002) Now that we can adjust argument explicitness in fields, we no longer need a custom delaborator.
fix: remove notation hacks in monoidal categories (#24002) Now that we can adjust argument explicitness in fields, we no longer need a custom delaborator.