Skip to content

Reorder legends#72

Open
user202729 wants to merge 1 commit intoPatrickMassot:masterfrom
user202729:legend-ordering
Open

Reorder legends#72
user202729 wants to merge 1 commit intoPatrickMassot:masterfrom
user202729:legend-ordering

Conversation

@user202729
Copy link
Copy Markdown

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