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

feat: add Lean language #1509

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

feat: add Lean language #1509

wants to merge 4 commits into from

Conversation

foxyseta
Copy link

Closes #1354.

Copy link
Collaborator

@spenserblack spenserblack left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I appreciate the creativity for this art!

While it looks fine in my terminal, it looks misaligned in GitHub. Looks like GitHub's monospace font doesn't play nicely with these characters (it improved when I forced GitHub to use my preferred monospace font). This makes me think that other monospace fonts that users might use won't have good compatibility with this art's characters. How do you feel about simplifying the art ( -> E, etc.)?

@foxyseta
Copy link
Author

Right. I assume GitH*b's monospace font is lacking those Unicode characters, and so a non-monospace fallback font is used. This could indeed also happen on terminals emulators whose monospace fonts collectively do not cover such characters.

I am not just using "E" for $\exists$ and "A" for $\forall$.

@foxyseta foxyseta requested a review from spenserblack January 16, 2025 08:18
Copy link
Collaborator

@spenserblack spenserblack left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@o2sh
Copy link
Owner

o2sh commented Jan 18, 2025

Thanks a lot for your contribution @foxyseta

I've adjusted your ASCII art to better resemble the original logo

image

What do you think?

    {0}       ______
    {0}|            |\              /|\       |
    {0}|            | \            / | \      |
    {0}|            |  \          /  |  \     |
    {0}|      ______|   \________/   |   \    |
    {0}|            |    \      /    |    \   |
    {0}|            |     \    /     |     \  |
    {0}|            |      \  /      |      \ |
    {0}|____________|       \/       |       \|

@foxyseta
Copy link
Author

Love it. You're so artsy😍

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Language request: Lean
3 participants