From e4f4cabc465ef4a3577637b2f7964c0c980ad20d Mon Sep 17 00:00:00 2001
From: "Anne C.A. Baanen" <vierkantor@vierkantor.com>
Date: Tue, 2 Dec 2025 11:10:36 +0100
Subject: [PATCH] chore(documentation.yaml): add Metaprogramming in Lean 4

This should be one of the primary sources on learning metaprogramming, so I sorted this with the other tutorial books like Theorem Proving in Lean 4 and the Hitchhiker's Guide.
---
 data/documentation.yaml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/data/documentation.yaml b/data/documentation.yaml
index 7c4dd0c50c..5b2bdd9d7c 100644
--- a/data/documentation.yaml
+++ b/data/documentation.yaml
@@ -183,6 +183,14 @@ documentation:
       - logic
       - metaprogramming
       - programming
+  - title: "Metaprogramming in Lean 4"
+    url: "https://leanprover-community.github.io/lean4-metaprogramming-book/"
+    description: "A full introduction to metaprogramming in Lean."
+    authors: Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat
+    accessed_at: 2025-12-02
+    category: tutorial
+    tags:
+      - metaprogramming
   - title: Mathlib API documentation
     url: "https://leanprover-community.github.io/mathlib4_docs/"
     description: "A complete listing of all definitions and theorems included with Mathlib."