🚧 This project is WORK IN PROGRESS. There are many TODOs to be done. Any report on typo, errors, and suggestions are welcome!
See https://github.com/alissa-tung/hacking-lean-in-lean-book
This material are initially purposed for a seminar about The Tactics in Lean4 hosted at BiCMR, Peking University. The scoped of this little book is hopefully some gentle introduction to functional programming using dependent typed programming languages, and meta programming with interactive theorem provers.