-
Notifications
You must be signed in to change notification settings - Fork 67
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Use box-drawing characters for character diagrams #1141
Labels
Comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I just realized this afternoon: why are we not using box-drawing characters for drawing our character diagrams? Agda-input:
---
.Here's a couple of rendered examples:
markdown
The first diagram is our current version of a commuting prism diagram, while the second diagram employs horizontal, vertical, and diagonal box-drawing characters. The third diagram demonstrates what the diagonals can look like with the right horizontal offset.
Note. It looks like there is a line spacing issue since the characters don't align perfectly, which they should by definition. This should also be fixed.
It seems to me that using box-drawing characters is objectively an improvement over our current convention, so I propose that we switch to using them. I am happy to back-implement this change if we agree it is better.
The text was updated successfully, but these errors were encountered: