The declaration read out of a def the package ships.

The certificate for a def the package ships.

The defs a package ships. Marking one reads the declaration out of it, so a declaration reaches the program only through the walk that proves what it denotes: there is no way to put an AST into a program by hand.

@[ship internal] ships the declaration without putting it in the API: other declarations call it, and it is named by neither the exports of index.js nor index.d.ts. It is the way to keep a helper out of the published surface without paying @[expand]'s fuel at every call site. The word is not private: Lean's own private takes the name out of the namespace, so the walk never sees the def at all, and it is what keeps a scaffolding lemma from shipping as a claim.

The mark is not @[export] either: Lean's own @[export] names a C symbol. A declaration taking a function stays internal whatever is written above it, because its type says so (Decl.isPublic).

Whether n is one of the defs the package ships.

The constants a package is made of: those declared directly in ns, in the order they were written. Private ones and the ones Lean generates are left out, which is how a helper stays out of the package.

One shipped def: the def itself, the declaration read out of it, and what that declaration is.

What ns ships, ordered so that every call goes backwards and otherwise in the order the defs were written.

The types ns declares, which are the ones deriving Enc wrote a TypeDef for.

Everything ns ships, above this point. The declarations are ordered so that every call goes backwards, and otherwise kept in the order they were written.