Definition catalogues

Every definition a source states, in the order it states them, with the section and page it appears on. A catalogue is the completeness check on the enumeration: what the book defines, before any question of Lean.