1.5. Reading this book🔗

This book is built with Verso. Its Lean code blocks are elaborated and type-checked as part of the book build, and displayed command output is checked against Lean's actual output. Hover over a highlighted name to see its type and declaration information.