|
|
|---|
|
|
|
|---|
Returns an alist associating book full pathnames with runes introduced
General Form: (book-runes-alist wrld) ; wrld an ACL2 logical world Typical Form: (book-runes-alist (w state))
This utility returns an alist. The keys are the full pathnames of books included in the given world. With such book is associated all runes introduced in that book — directly introduced, rather than being introduced in an included sub-book. The computation is made efficient by use of memoization (see memoize).