This report describes the current LEGO library, which was designed as a basis upon which users can develop their own work, and also some example proof developments using this library. An earlier version of the library was developed by Savi Maharaj for use by students being introduced to the LEGO system . We hope that this version will provide useful preliminaries for all users. We have received contributions from: Thorsten Altenkirch ; Petr Cizek; Adriana Compagnoni; Healf Goguen ; Martin Hofmann ; Claire Jones; Zhaohui Luo ; Savi Maharaj; Conor McBride ; James McKinna ; Randy Pollack ; Thomas Schreiber . The LEGO library contains around 250 definitions and 400 theorems, and covers both the common datatypes such as natural numbers, list, booleans, products, sums, unit, empty and some more unusual ones such as integers, sigma types, quotient types, finite sets, vectors. New modules have been incorporated offering
Makecommand in LEGO.