Blueprint Lean Code Link Preview Wiring

Blueprint Summary🔗

Overview
Total entries17completed: 3; deps incomplete: 0; sorries: 2; no proof: 5
Ready now11Entries with an actionable next formalization step.
Fully closed3Local code and prerequisite closure are both complete.
Actionable priorities6Entries ready now and already unlocking downstream work.
Current blockers2Missing external or incomplete Lean declarations.
Actionable priorities (6)
  • «def:preview.base»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:used.single»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:uses.hidden»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:uses.inline»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:uses.proof.extra»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:uses.proof»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
Current blockers (2)
  • «def:status.axiom»(Definition)
    Axiom-like declaration: Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusAxiom [definition; axiom-like; axiom-like (no body); refs: n/a]
  • «def:status.sorry»(Definition)
    Declaration with sorry: Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusSorry [theorem/lemma; contains sorry; in proof; refs: 1]
Entry index (17)
Definitions12completed: 3; deps incomplete: 0; sorries: 2; no proof: 0
Lemmas3completed: 0; deps incomplete: 0; sorries: 0; no proof: 3
Theorems2completed: 0; deps incomplete: 0; sorries: 0; no proof: 2
Axiom-like entries1completed: 0; deps incomplete: 0; sorries: 1; no proof: 0
Informal-only entries12
Definition Index (12)
  • «def:uses.hidden»(Definition)
  • «def:uses.inline»(Definition)
  • «def:preview.base»(Definition)
  • «def:status.proved»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusProved
  • «def:uses.proof.extra»(Definition)
  • «def:status.axiom»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusAxiom
  • «def:status.sorry»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusSorry
  • «def:used.target»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.usedByPreviewTarget
  • «def:uses.proof»(Definition)
  • «def:used.single»(Definition)
  • «def:status.none»(Definition)
  • «def:code.preview»(Definition)
    Associated lean decls (1)
Theorem / Proposition / Lemma / Corollary Index (5)
  • «lem:used.statement»(Lemma)
  • «thm:uses.panel»(Theorem)
  • «lem:used.single.next»(Lemma)
  • «lem:preview.next»(Lemma)
  • «thm:used.proof»(Theorem)
Axiom-like Index (1)
  • «def:status.axiom»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusAxiom
Dependency insights
Statement-used entries5Entries reused in statement dependencies.
Proof-used entries3Entries reused in proof-only dependencies.
Most used in statements (5)
  • «def:used.target»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.usedByPreviewTarget
  • «def:preview.base»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:used.single»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:uses.hidden»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:uses.inline»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Most used in proofs (3)
  • «def:used.target»(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.usedByPreviewTarget
  • «def:uses.proof.extra»(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  • «def:uses.proof»(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Metadata
Metadata audit
Missing owner17
Missing effort17
Untagged17
Missing owner (17)
  • «def:code.preview»(Definition)
    Missing owner metadata.
    Associated lean decls (1)
  • «def:preview.base»(Definition)
    Missing owner metadata.
  • «def:status.axiom»(Definition)
    Missing owner metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusAxiom
  • «def:status.none»(Definition)
    Missing owner metadata.
  • «def:status.proved»(Definition)
    Missing owner metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusProved
  • «def:status.sorry»(Definition)
    Missing owner metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusSorry
  • «def:used.single»(Definition)
    Missing owner metadata.
  • «def:used.target»(Definition)
    Missing owner metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.usedByPreviewTarget
  • «def:uses.hidden»(Definition)
    Missing owner metadata.
  • «def:uses.inline»(Definition)
    Missing owner metadata.
  • Show all 7 more entries missing owner
    • «def:uses.proof.extra»(Definition)
      Missing owner metadata.
    • «def:uses.proof»(Definition)
      Missing owner metadata.
    • «lem:preview.next»(Lemma)
      Missing owner metadata.
    • «lem:used.single.next»(Lemma)
      Missing owner metadata.
    • «lem:used.statement»(Lemma)
      Missing owner metadata.
    • «thm:used.proof»(Theorem)
      Missing owner metadata.
    • «thm:uses.panel»(Theorem)
      Missing owner metadata.
Missing effort (17)
  • «def:code.preview»(Definition)
    Missing effort metadata.
    Associated lean decls (1)
  • «def:preview.base»(Definition)
    Missing effort metadata.
  • «def:status.axiom»(Definition)
    Missing effort metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusAxiom
  • «def:status.none»(Definition)
    Missing effort metadata.
  • «def:status.proved»(Definition)
    Missing effort metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusProved
  • «def:status.sorry»(Definition)
    Missing effort metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusSorry
  • «def:used.single»(Definition)
    Missing effort metadata.
  • «def:used.target»(Definition)
    Missing effort metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.usedByPreviewTarget
  • «def:uses.hidden»(Definition)
    Missing effort metadata.
  • «def:uses.inline»(Definition)
    Missing effort metadata.
  • Show all 7 more entries missing effort
    • «def:uses.proof.extra»(Definition)
      Missing effort metadata.
    • «def:uses.proof»(Definition)
      Missing effort metadata.
    • «lem:preview.next»(Lemma)
      Missing effort metadata.
    • «lem:used.single.next»(Lemma)
      Missing effort metadata.
    • «lem:used.statement»(Lemma)
      Missing effort metadata.
    • «thm:used.proof»(Theorem)
      Missing effort metadata.
    • «thm:uses.panel»(Theorem)
      Missing effort metadata.
Untagged (17)
  • «def:code.preview»(Definition)
    Missing tag metadata.
    Associated lean decls (1)
  • «def:preview.base»(Definition)
    Missing tag metadata.
  • «def:status.axiom»(Definition)
    Missing tag metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusAxiom
  • «def:status.none»(Definition)
    Missing tag metadata.
  • «def:status.proved»(Definition)
    Missing tag metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusProved
  • «def:status.sorry»(Definition)
    Missing tag metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusSorry
  • «def:used.single»(Definition)
    Missing tag metadata.
  • «def:used.target»(Definition)
    Missing tag metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.usedByPreviewTarget
  • «def:uses.hidden»(Definition)
    Missing tag metadata.
  • «def:uses.inline»(Definition)
    Missing tag metadata.
  • Show all 7 more untagged entries
    • «def:uses.proof.extra»(Definition)
      Missing tag metadata.
    • «def:uses.proof»(Definition)
      Missing tag metadata.
    • «lem:preview.next»(Lemma)
      Missing tag metadata.
    • «lem:used.single.next»(Lemma)
      Missing tag metadata.
    • «lem:used.statement»(Lemma)
      Missing tag metadata.
    • «thm:used.proof»(Theorem)
      Missing tag metadata.
    • «thm:uses.panel»(Theorem)
      Missing tag metadata.
Structure and coverage
Informal-only12Statements with no associated Lean code yet.
Ready to formalize11Entries with an actionable next formalization step.
Fully closed3Local code and ancestor closure are both complete.
Blocked or incomplete3Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (5)
  • «thm:uses.panel»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 2proof deps: 2direct uses: 0downstream unlocks: 0
  • «thm:used.proof»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  • «lem:preview.next»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  • «lem:used.single.next»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  • «lem:used.statement»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
No prerequisites (12)
  • «def:preview.base»(Definition)
  • «def:status.axiom»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusAxiom
  • «def:status.sorry»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusSorry
  • «def:used.target»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.usedByPreviewTarget
  • «def:uses.proof»(Definition)
  • «def:code.preview»(Definition)
    Associated lean decls (1)
  • «def:status.none»(Definition)
  • «def:used.single»(Definition)
  • «def:uses.proof.extra»(Definition)
  • «def:status.proved»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusProved
  • Show all 2 more entries without prerequisites
    • «def:uses.inline»(Definition)
    • «def:uses.hidden»(Definition)
No dependents (10)
  • «lem:used.statement»(Lemma)
  • «thm:uses.panel»(Theorem)
  • «lem:preview.next»(Lemma)
  • «def:status.axiom»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusAxiom
  • «def:status.sorry»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusSorry
  • «thm:used.proof»(Theorem)
  • «def:code.preview»(Definition)
    Associated lean decls (1)
  • «def:status.none»(Definition)
  • «def:status.proved»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.Shared.previewStatusProved
  • «lem:used.single.next»(Lemma)