Summary Blockers🔗

Compiled2026-05-06T13:19:15ZProject 5480f6aMerge pull request #37 from leanprover/feat/reference-catalog-pagesLeanleanprover/lean4:v4.30.0-rc2VersoBlueprint 5480f6a

Definition2

!L∃∀Nused by 0

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

⚠L∃∀Nused by 0

Inline sorry sample.

Lean code for Definition3

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

Blueprint Summary

Summary Blockers🔗

Contents