From 587530755a7a44625e570938a161d7aa1dc612dc Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Thu, 13 Feb 2025 19:41:01 +0100
Subject: [PATCH] feat: add link tactic list (#591)

Add a link to the Verso project [Mathlib
Manual](https://leanprover-community.github.io/mathlib-manual/html-multi/),
currently featuring an auto-generated list of all tactics, along with
some curated tactic lists.
---
 data/menus.yaml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/data/menus.yaml b/data/menus.yaml
index 25351c981..530932519 100644
--- a/data/menus.yaml
+++ b/data/menus.yaml
@@ -21,6 +21,7 @@
     - Learning resources (start here): learn.html
     - API documentation: https://leanprover-community.github.io/mathlib4_docs
     - Declaration search (Loogle): https://loogle.lean-lang.org/
+    - Tactic list: https://leanprover-community.github.io/mathlib-manual/html-multi/
     - Calc mode: extras/calc.html
     - Conv mode: extras/conv.html
     - Simplifier: extras/simp.html