Vocabulary written where it is called #

A def marked @[expand] is not a declaration the package ships. The walk replaces a call to it with its body, so what reaches Core.Expr is the forms the body is built out of and nothing else.

That is what lets the vocabulary be polymorphic. Core.Decl has a List Param and a Ty, and no type parameters, so Arr.take : List α → Int → List α has no declaration to be read out into; at a call site α is already Int or String, and the expansion is a term the walk can read. The cost is that the generated module has no function for it: the body appears at each call, and the fuel the program needs grows with it.

Prelude.lean is where the library's own marked defs live. The mark is open to an author as well: a helper used by several shipped defs but not meant to cross the boundary carries it, and stays out of index.d.ts and the exports because it stays out of the program.