Lean 4 (Meta)programming Cookbook
Lean 4 (Meta)programming Cookbook
Table of Contents
What is Metaprogramming?
Syntax and Macros
Working with Expressions
Elaboration for Syntax
Tactics
File System
Data Structures
I/O and Processes
Maintaining state
Index
How to build a Recipe
Cookbook Contributors
Working with Expressions
Types of Expressions
Displaying in the Infoview
Syntax strings from expressions
Exact Pattern-Matching
Pattern-Matching by Solving
Expressions for function applications
Building expressions with variables, functions, and dependent function types
Replacing code using
TryThis
Replacing code using
TryThis
←
Building expressions with variables, functions, and dependent function types
Elaboration for Syntax
→
Replacing code using
TryThis
🔗
←
Building expressions with variables, functions, and dependent function types
Elaboration for Syntax
→
