Summary Blockers🔗

Compiled2026-07-17T18:20:11ZProject 51ebcaeMerge pull request #348 from leanprover/feat/fix-graph-data-topologyLeanleanprover/lean4:v4.32.0VersoBlueprint 51ebcae

Definition2

uses 0used by 0!L∃∀N

Missing external declaration sample.

Lean code for Definition2●1 declaration, 1 missing

Nat.nopemissing declaration

declaration not found (name was not present during directive/code-block registration)

Definition3

uses 0used by 0⚠L∃∀N

Inline sorry sample.

Lean code for Definition3

theorem declaration uses `sorry`summaryBlockerSorry : True := by⊢ True
  sorryAll goals completed! 🐙

Blueprint Summary

Summary Blockers🔗

Contents