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`

←Adding syntax (categories)Types of Expressions→

Working with Expressions🔗

Contributors: Siddhartha Gadgil

In this chapter we collect recipes to manipulate expressions including building and pattern-matching.

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

←Adding syntax (categories)Types of Expressions→