lean-ja · Seasawher · Sep 17, 2024 · Sep 17, 2024
@@ -1,5 +1,5 @@
 /- # app_unexpander
-`app_unexpander` 属性を付与すると、関数適用 `f a₁ a₂ ... aₙ` の `#check` コマンドおよび infoview での表示のされ方を変更することができます。
+`[app_unexpander]` 属性を付与すると、関数適用 `f a₁ a₂ ... aₙ` の `#check` コマンドおよび infoview での表示のされ方を変更することができます。
 -/
 namespace AppUnexpander --#
 

@@ -1,8 +1,8 @@
 /- # cases_eliminator
 
-`cases_eliminator` 属性は、[`cases`](../../Tactic/Cases.md) タクティクで場合分けをした際の枝を変更します。
+`[cases_eliminator]` 属性は、[`cases`](../../Tactic/Cases.md) タクティクで場合分けをした際の枝を変更します。
 
-より詳しくいうと、[`cases`](../../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`cases_eliminator` 属性で別な定理を指定すると、それが使われるようになります。
+より詳しくいうと、[`cases`](../../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[cases_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
 -/
 namespace CasesEliminator --#
 
@@ -35,7 +35,7 @@ info: CasesEliminator.Many.casesOn.{u} {α : Type} {motive : Many α → Sort u}
 #guard_msgs (whitespace := lax) in #check Many.casesOn
 
 /-- Many.casesOn の more を cons に置き換えたバージョン。
-この定理に `cases_eliminator` 属性を与えることで、
+この定理に `[cases_eliminator]` 属性を与えることで、
 `casesOn` の代わりにこれがデフォルトで使われるようになる。 -/
 @[cases_eliminator]
 protected def Many.cons_casesOn.{u} {α : Type} {motive : Many α → Sort u} (t : Many α) (none : motive Many.none)

@@ -1,5 +1,5 @@
 /- # csimp
-`csimp` は、コンパイラに単純化を指示する属性です。
+`[csimp]` 属性は、コンパイラに単純化を指示します。
 
 `A = B` という形の定理に付与することでコンパイラに `A` の計算を `B` の計算に置き換えさせることができます。非効率な関数を効率的な実装に置き換えるために使用されます。
 -/
@@ -44,7 +44,7 @@ where
 theorem fib_add (n : Nat) : fib (n + 2) = fib n + fib (n + 1) := by rfl
 
 /-- `fibonacci` と `fib` は同じ結果を返す。
-`csimp` 属性を与えることで、`fibonacci` の計算を `fib` の計算に置き換えることができる。-/
+`[csimp]` 属性を与えることで、`fibonacci` の計算を `fib` の計算に置き換えることができる。-/
 @[csimp]
 theorem fib_eq_fibonacci : fibonacci = fib := by
   ext n

@@ -1,8 +1,8 @@
 /- # induction_eliminator
 
-`induction_eliminator` 属性は、帰納法の枝を変更することを可能にします。
+`[induction_eliminator]` 属性は、帰納法の枝を変更することを可能にします。
 
-より詳しくいうと、[`induction`](../../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`induction_eliminator` 属性で別な定理を指定すると、それが使われるようになります。
+より詳しくいうと、[`induction`](../../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[induction_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
 -/
 namespace InductionEliminator --#
 
@@ -42,7 +42,7 @@ info: InductionEliminator.Many.rec.{u} {α : Type} {motive : Many α → Sort u}
 #guard_msgs (whitespace := lax) in #check Many.rec
 
 -- Many.rec の `Many.more` の部分を `Many.cons` に置き換えた定理を作る。
--- これに `induction_eliminator` 属性を与えることで、
+-- これに `[induction_eliminator]` 属性を与えることで、
 -- コンストラクタ `Many.more` の代わりに `Many.cons` が使えるようになる
 @[induction_eliminator]
 protected def Many.cons_rec.{u} {α : Type} {motive : Many α → Sort u}

@@ -1,5 +1,5 @@
 /- # inherit_doc
-`inherit_doc` 属性を指定すると、既存の定数などのドキュメントコメントを使いまわすことができます。
+`[inherit_doc]` 属性を指定すると、既存の定数などのドキュメントコメントを使いまわすことができます。
 -/
 import Lean
 

@@ -1,6 +1,6 @@
 /- # match_pattern
 
-`match_pattern` 属性を付与すると、元々コンストラクタしか使用できない `match` 式でのパターンマッチの枝に、指定した関数を使うことができるようになります。
+`[match_pattern]` 属性を付与すると、元々コンストラクタしか使用できない `match` 式でのパターンマッチの枝に、指定した関数を使うことができるようになります。
 -/
 
 /-- 自前で定義したリスト -/
@@ -21,7 +21,7 @@ def MyList.myCons (a : α) (as : MyList α) : MyList α :=
     | MyList.nil => 0
     | MyList.myCons _ as => 1 + badLength as
 
--- `match_pattern` 属性を付与する
+-- `[match_pattern]` 属性を付与する
 attribute [match_pattern] MyList.myCons
 
 -- これで `match` の中で `MyList.myCons` を使うことができる

@@ -1,8 +1,8 @@
 /- # simps
 
-補題を [`simp`](../../Tactic/Simp.md) で使えるようにするのは `@[simp]` タグを付けることで可能ですが、`simps` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。
+補題を [`simp`](../../Tactic/Simp.md) で使えるようにするのは `[simp]` 属性を付与することで可能ですが、`[simps]` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。
 
-例えば、ユーザが `Point` という構造体を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`simps` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
+例えば、ユーザが `Point` という構造体を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
 -/
 import Mathlib.Tactic.Simps.Basic -- simps 属性を使うため
 
@@ -22,7 +22,7 @@ example (a b : Point) : (Point.add a b).x = a.x + b.x := by
 
   rfl
 
--- `Point.add` に `simps` 属性を付与する
+-- `Point.add` に `[simps]` 属性を付与する
 attribute [simps] Point.add
 
 example (a b : Point) : (Point.add a b).x = a.x + b.x := by

@@ -30,7 +30,7 @@ abbrev NaturalNumber : Type := Nat
 
 end Abbrev1 --#
 /- ## 舞台裏
-`abbrev` は `@[reducible]` 属性のついた `def` と同じであり、定義に `reducible` という属性を与えても同様のことができます。-/
+`abbrev` は `[reducible]` 属性のついた `def` と同じであり、定義に `[reducible]` 属性を与えても同様のことができます。-/
 namespace Abbrev2 --#
 
 @[reducible] def NaturalNumber : Type := Nat

@@ -3,7 +3,7 @@
 
 `attribute` は、属性(attribute)を付与するためのコマンドです。
 
-次の例では、命題に `simp` 属性を付与しています。これは `simp` タクティクで利用される命題を増やすことを意味します。
+次の例では、命題に `[simp]` 属性を付与しています。これは `simp` タクティクで利用される命題を増やすことを意味します。
 -/
 namespace Attribute --#
 
@@ -34,7 +34,7 @@ example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
 /- ## 属性の削除
 与えた属性を削除することができることもあります。削除するには `-` を属性の頭に付けます。-/
 section
-  -- `simp` 属性を削除
+  -- `[simp]` 属性を削除
   attribute [-simp] foo
 
   -- 再び示せなくなった

@@ -69,7 +69,7 @@ instance {n : Nat} [OfNat Even n] : OfNat Even (n + 2) where
 
 /-
 ## 舞台裏
-`instance` は `@[instance]` 属性を付与された [`def`](./Def.md) と同じようにはたらきます。ただし `instance` はインスタンス名を省略することができるという違いがあります。
+`instance` は `[instance]` 属性を付与された [`def`](./Def.md) と同じようにはたらきます。ただし `instance` はインスタンス名を省略することができるという違いがあります。
 -/
 
 -- `List` 同士を足すことはできない

@@ -27,7 +27,7 @@ example : s ∩ t = t ∩ s := by
   aesop
 
 /- ## ext 属性
-`ext` 属性を命題に与えると、上記のようにその命題は `ext` タクティクで利用できるようになります。さらに、`ext` 属性は構造体に対しても与えることができます。このとき、その構造体に対して自動的に `.ext` と `.ext_iff` の２つの定理が生成されます。
+`[ext]` 属性を命題に与えると、上記のようにその命題は `ext` タクティクで利用できるようになります。さらに、`[ext]` 属性は構造体に対しても与えることができます。このとき、その構造体に対して自動的に `.ext` と `.ext_iff` の２つの定理が生成されます。
 -/
 
 variable {α : Type}
@@ -40,7 +40,7 @@ structure Point (α : Type) where
 #check_failure Point.ext
 #check_failure Point.ext_iff
 
--- `Point` に `ext` 属性を与える
+-- `Point` に `[ext]` 属性を与える
 attribute [ext] Point
 
 -- 自動生成された定理

@@ -43,7 +43,7 @@ example {c d : ℝ} (h : a + c + 1 ≤ b + d + 1) :
   linarith
 
 /-! ## 補題の登録
-さらに `@[gcongr]` という属性(attribute)を付与することにより、 `gcongr` で呼び出して使える補題を増やすことができます。-/
+さらに `[gcongr]` 属性を付与することにより、 `gcongr` で呼び出して使える補題を増やすことができます。-/
 
 variable {U : Type*}
 variable (A B C : Set U)