Closed fredrik-bakke closed 5 months ago
The font size in agda code blocks is larger than in other code blocks.
Inspection reveals that Agda code is displayed with a font size of 15.68px, while text blocks are displayed with a font size of 13.72px:
vs.
Personally, I think it looks a little better with the slightly smaller size.
The font size in agda code blocks is larger than in other code blocks.
Inspection reveals that Agda code is displayed with a font size of 15.68px, while text blocks are displayed with a font size of 13.72px:
vs.
Personally, I think it looks a little better with the slightly smaller size.