Skip to content

Reorder legends #72

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

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

user202729
Copy link

The current legend content is like

Boxes:
    definitions
Ellipses:
    theorems and lemmas
Blue border:
    the statement of this result is ready to be formalized; all prerequisites are done
Orange border:
    the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background:
    the proof of this result is ready to be formalized; all prerequisites are done
Green border:
    the statement of this result is formalized
Green background:
    the proof of this result is formalized
Dark green background:
    the proof of this result and all its ancestors are formalized
Dark green border:
    this is in Mathlib

I find the ordering very confusing.

The new ordering is such that it lists all border entries before the background entries, and in order of increasing completion.


Actually I prefer something like this

Boxes:
    definitions
Ellipses:
    theorems and lemmas
Border:
    Orange:
        the statement of this result is not ready to be formalized; the blueprint needs more work
    Blue:
        the statement of this result is ready to be formalized; all prerequisites are done
    Green:
        the statement of this result is formalized
    Dark green:
        this is in Mathlib
Background:
    Blue:
        the proof of this result is ready to be formalized; all prerequisites are done
    Green:
        the proof of this result is formalized
    Dark green:
        the proof of this result and all its ancestors are formalized

but that appears to require a little more work to implement the three-level hierarchy.

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.

1 participant