Lambda Calculus in Lean🔗

This book develops lambda calculi as object languages inside Lean. The chapters below are the actual Lean source files rendered as literate pages. The book is therefore a table of contents and publishing layer for the course files, not a second copy of their content.