Blueprint Summary
Overview
Total entries3completed: 1; deps incomplete: 0; sorries: 1; no proof: 0
Ready now2Entries whose next formalization step is currently unblocked.
Fully closed1Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Current blockers2Missing external or incomplete Lean declarations.
Current blockers (2)
-
Missing external Lean declaration:
Nat.nope[missing declaration] -
Declaration with sorry:
Verso.VersoBlueprintTests.BlueprintSummaryLinks.Shared.summaryBlockerSorry[theorem/lemma; contains sorry; in proof; refs: 1]
Entry index (3)
Definitions3completed: 1; deps incomplete: 0; sorries: 1; no proof: 0
Definition Index (3)
-
Associated lean decls (1)
-
«def:external.summary»Associated lean decls (1)
-
Nat.add
-
-
Associated lean decls (1)
Metadata
Metadata audit
Missing owner3
Missing effort3
Untagged3
Missing owner (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
«def:external.summary»Missing owner metadata.Associated lean decls (1)
-
Nat.add
-
Missing effort (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
«def:external.summary»Missing effort metadata.Associated lean decls (1)
-
Nat.add
-
Untagged (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
«def:external.summary»Missing tag metadata.Associated lean decls (1)
-
Nat.add
-
Structure and coverage
Ready to formalize2Entries whose next step is currently unblocked.
Fully closed1Local code and ancestor closure are both complete.
No prerequisites (3)
-
Associated lean decls (1)
-
«def:external.summary»Associated lean decls (1)
-
Nat.add
-
-
Associated lean decls (1)
No dependents (3)
-
Associated lean decls (1)
-
«def:external.summary»Associated lean decls (1)
-
Nat.add
-
-
Associated lean decls (1)