From 5d6b4639a8b90ad746bc7eeda9018f6e5b8117a3 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Fri, 22 Nov 2024 21:58:05 +0900 Subject: [PATCH] =?UTF-8?q?=E7=BF=BB=E8=A8=B3=E9=96=8B=E5=A7=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Manual/Simp.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Manual/Simp.lean b/Manual/Simp.lean index bc2784f..b55cea2 100644 --- a/Manual/Simp.lean +++ b/Manual/Simp.lean @@ -16,7 +16,10 @@ set_option pp.rawOnError true set_option linter.unusedVariables false +/- #doc (Manual) "The Simplifier" => +-/ +#doc (Manual) "単純化器(The Simplifier)" => %%% tag := "the-simplifier" %%%