Skip to content

Commit

Permalink
Mathlib #help の出力へのリンクが間違っていたので修正する
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Nov 13, 2024
1 parent 40a53d5 commit b10bb78
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion LeanByExample/Reference/Attribute/README.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
属性は、`attribute [foo] bar` または `@[foo]` という構文で使用することができます。
Mathlib において利用可能な属性の一覧は [attribute list](https://seasawher.github.io/mathlib4-help/attributes.html) で確認できます。
Mathlib において利用可能な属性の一覧は [attribute list](https://seasawher.github.io/mathlib4-help/attributes/) で確認できます。
-/
2 changes: 1 addition & 1 deletion LeanByExample/Reference/Tactic/README.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,5 +3,5 @@
このセクションでは、Lean の組み込みのタクティクに加えて、Mathlib というライブラリで提供されているタクティクも紹介します。Mathlib には特定の分野に特化した強力な自動化タクティクがいくつもあり、数学理論の形式化をする上で欠かせません。
なおこのリストは全部のタクティクを網羅していません。Mathlib の全タクティクのリストが必要であれば [mathlib4 tactics](https://seasawher.github.io/mathlib4-help/tactics.html) を参照してください。
なおこのリストは全部のタクティクを網羅していません。Mathlib の全タクティクのリストが必要であれば [mathlib4 tactics](https://seasawher.github.io/mathlib4-help/tactics/) を参照してください。
-/

0 comments on commit b10bb78

Please sign in to comment.