Summary Blockers

 Summary Blockers🔗

Compiled2026-07-01T21:39:40ZProject5f17f8aMerge pull request #222 from leanprover/chore/reference-blueprints-catalog-all-v4.30.0-v4.31.0Leanleanprover/lean4:v4.31.0VersoBlueprint5f17f8a
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 Definition3theorem declaration uses `sorry`summaryBlockerSorry : True := ⊢ True All goals completed! 🐙

Contents

  1. Blueprint Summary