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
Tactics
Hello World Tactic
Tactic using macros
Tactics using elaborators
Tactics as abbreviations and mnemonics
Checking validity of Tactics
Tactics closing goals
Tactics giving new goals.
trying different natural numbers
Tactic using macros
repeat_apply
tactic
←
A Basic Tactic
repeat_apply tactic
→
Tactic using macros
🔗
Contributors:
ajay-k-nair
repeat_apply
tactic
←
A Basic Tactic
repeat_apply tactic
→
