5480f6a
Nat.nope
Missing external declaration sample.
declaration not found (name was not present during directive/code-block registration)
Verso.VersoBlueprintTests.BlueprintSummaryLinks.Shared.summaryBlockerSorry
Inline sorry sample.
theorem declaration uses `sorry`summaryBlockerSorry : True := by⊢ True sorryAll goals completed! 🐙
declaration uses `sorry`