Distinct from LEAN_PACKAGES.length === 0, and the distinction is the point:
a folio may legitimately declare no Lean packages, and that is a different
answer from nobody having declared anything. A caller that cannot resolve a
lean.ref should say which of the two it is.
Whether a folio has configured the registry.
Distinct from
LEAN_PACKAGES.length === 0, and the distinction is the point: a folio may legitimately declare no Lean packages, and that is a different answer from nobody having declared anything. A caller that cannot resolve alean.refshould say which of the two it is.