(Meta)programming in Lean4 Cookbook

A cookbook containing recipes(code snippets) for both programming and metaprogramming in Lean4. Visit the website to read the cookbook.

This repository does not contain any recipes for proving in mathematics, it is only focused on (meta)programming in Lean4.

[!Important] This repository is under development and we are working hard to add more recipes to it. If you have any recipes that you would like to contribute, please feel free to create a pull request.

[!Note] This repository is not a book and it may not always explain concepts particular to a concept. It is just a collection of recipes that can help you in your coding journey. It is recommended that you clear your concepts from other books and resources of Lean4.

Motivation for Cookbook

It's like a cheatsheet, IT IS VERY USEFUL!

Getting Started

If you are new to Lean4 and (meta)programming, we recommend you to start with basics of Lean4 clearing your basics from resources like MIL, TPIL, FPIL, etc. This will help you understand the recipes in this repository better. You can also use this repository for learning purposes by seeing simple snippets and practically using them in your code.

For the audience familiar with Lean4, you can directly visit the website, and search for the recipes that you are looking for. You can also contribute to the repository by adding new recipes or improving existing ones.

Contributing

This repository is very much under development and we would welcome your contributions. This contributions must follow the contributing guidelines and your code should be specific format as mentioned in the Cookbook guidelines.

Please create a pull request with your code snippet and we will review it as soon as possible.

Acknowledgements

This is an initiative to help everyone learn metaprogramming in Lean4 and we would like to thank everyone from the Lean4 community who has contributed to this repository.

This repository is built using Verso.