Merge pull request #732 from lean-ja/attribute

属性リストへのリンクを追加する
lean-ja · Aug 31, 2024 · 54a135b · 54a135b
2 parents 79ac962 + 5ad35ba
commit 54a135b
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git 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
@@ -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) を参照してください。
 -/