From 5ad35ba13f962da25e6420acc08750f0c363b329 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 1 Sep 2024 07:14:28 +0900 Subject: [PATCH] =?UTF-8?q?=E5=B1=9E=E6=80=A7=E3=83=AA=E3=82=B9=E3=83=88?= =?UTF-8?q?=E3=81=B8=E3=81=AE=E3=83=AA=E3=83=B3=E3=82=AF=E3=82=92=E8=BF=BD?= =?UTF-8?q?=E5=8A=A0=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Command/Attribute/README.lean | 7 ++++++- Examples/Tactic/README.lean | 2 +- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/Examples/Command/Attribute/README.lean b/Examples/Command/Attribute/README.lean index 13f30215..10527cc3 100644 --- a/Examples/Command/Attribute/README.lean +++ b/Examples/Command/Attribute/README.lean @@ -1 +1,6 @@ -/- # 属性 -/ +/- # 属性 + +属性は、`attribute [foo] bar` または `@[foo]` という構文で使用することができます。 + +Mathlib において利用可能な属性の一覧は [attribute list](https://seasawher.github.io/mathlib4-tactics/attributes.html) で確認できます。 +-/ diff --git a/Examples/Tactic/README.lean b/Examples/Tactic/README.lean index 7f8d46d5..b4a0174b 100644 --- a/Examples/Tactic/README.lean +++ b/Examples/Tactic/README.lean @@ -3,5 +3,5 @@ このセクションでは、Lean の組み込みのタクティクに加えて、Mathlib というライブラリで提供されているタクティクも紹介します。Mathlib には特定の分野に特化した強力な自動化タクティクがいくつもあり、数学理論の形式化をする上で欠かせません。 -なおこのリストは全部のタクティクを網羅していません。Mathlib の全タクティクのリストが必要であれば [mathlib4 tactics](https://seasawher.github.io/mathlib4-tactics) を参照してください。 +なおこのリストは全部のタクティクを網羅していません。Mathlib の全タクティクのリストが必要であれば [mathlib4 tactics](https://seasawher.github.io/mathlib4-tactics/tactics.html) を参照してください。 -/