diff --git a/leanblueprint/Packages/blueprint.py b/leanblueprint/Packages/blueprint.py index dc83348..193ea4a 100644 --- a/leanblueprint/Packages/blueprint.py +++ b/leanblueprint/Packages/blueprint.py @@ -297,20 +297,20 @@ def make_legend() -> None: descriptions. """ document.userdata['dep_graph']['legend'].extend([ - (f"{document.userdata['dep_graph']['colors']['can_state'][1]} border", - "the statement of this result is ready to be formalized; all prerequisites are done"), (f"{document.userdata['dep_graph']['colors']['not_ready'][1]} border", "the statement of this result is not ready to be formalized; the blueprint needs more work"), - (f"{document.userdata['dep_graph']['colors']['can_state'][1]} background", - "the proof of this result is ready to be formalized; all prerequisites are done"), + (f"{document.userdata['dep_graph']['colors']['can_state'][1]} border", + "the statement of this result is ready to be formalized; all prerequisites are done"), (f"{document.userdata['dep_graph']['colors']['proved'][1]} border", "the statement of this result is formalized"), + (f"{document.userdata['dep_graph']['colors']['mathlib'][1]} border", + "this is in Mathlib"), + (f"{document.userdata['dep_graph']['colors']['can_state'][1]} background", + "the proof of this result is ready to be formalized; all prerequisites are done"), (f"{document.userdata['dep_graph']['colors']['proved'][1]} background", "the proof of this result is formalized"), (f"{document.userdata['dep_graph']['colors']['fully_proved'][1]} background", "the proof of this result and all its ancestors are formalized"), - (f"{document.userdata['dep_graph']['colors']['mathlib'][1]} border", - "this is in Mathlib"), ]) document.addPostParseCallbacks(150, make_legend)