Skip to content
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

Glyph request: ∘ (U+2218) #1536

Open
glatavento opened this issue Jun 14, 2023 · 3 comments
Open

Glyph request: ∘ (U+2218) #1536

glatavento opened this issue Jun 14, 2023 · 3 comments
Labels
Milestone

Comments

@glatavento
Copy link

which is used to represent function composition in agda.

@tonsky
Copy link
Owner

tonsky commented Jun 14, 2023

Is this enough for agda or does it require a lot of other symbols too?

@glatavento
Copy link
Author

Is this enough for agda or does it require a lot of other symbols too?

A lot, I am afraid. Agda uses almost every math symbols. To give you an idea of the scale, I ran the command rg -oNI "[^\x00-\x7F]" | sort | uniq -c | sort -nr on Agda's standard library and here is the result. The Mononoki font (https://madmalik.github.io/mononoki/) includes the most frequently used symbols.

While Agda uses such a wide variety of symbols, is one that's also used in other languages or texts and cannot be easily replaced with other symbols. For example, can be replaced by >-, but is not as easily replaceable.

(I'm a newbie in agda so what I say may be inaccurate or incorrect; Thanks a lot for creating this font, I've been using it for years)

@tonsky
Copy link
Owner

tonsky commented Jun 19, 2023

Ok thanks! Let’s start small

@tonsky tonsky added this to the 7 milestone Jun 19, 2023
@tonsky tonsky added the Unicode label Jun 19, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants