Operators翻訳

Manual/NotationsMacros.lean

@@ -428,7 +428,7 @@ Term quotation has a higher priority than command quotation, so the quotation is
 Terms expect their {tech}[antiquotations] to have type {lean}``TSyntax `term`` rather than {lean}``TSyntax `command``.
 :::
 
-以下の例では、quotation の中身は関数適用かコマンド列のどちらかです。どちらもファイルの同じ領域でマッチするため、 {tech}[local longest-match rule] は関係しません。項の quotation はコマンドの quotation よりも優先順位が高いため、quotation は項として解釈されます。項は {lean}``TSyntax `command`` 型よりも {lean}``TSyntax `term`` 型を持つ {tech}[antiquotations] を期待します。
+以下の例では、quotation の中身は関数適用かコマンド列のどちらかです。どちらもファイルの同じ領域でマッチするため、 {tech}[ローカル最長一致規則] は関係しません。項の quotation はコマンドの quotation よりも優先順位が高いため、quotation は項として解釈されます。項は {lean}``TSyntax `command`` 型よりも {lean}``TSyntax `term`` 型を持つ {tech}[antiquotations] を期待します。
 
 ```lean (error := true) (name := cmdQuot)
 example (cmd1 cmd2 : TSyntax `command) : MacroM (TSyntax `command) := `($cmd1 $cmd2)

Manual/NotationsMacros/Notations.lean

@@ -92,7 +92,7 @@ If this still does not resolve the ambiguity, then all are saved, and the elabor
 
 :::
 
-演算子と同様に、 {tech}[local longest-match rule] が記法をパースする際に使用されます。もし複数の記法が最長一致で並んだ場合、宣言された優先順位によってどのパース結果が適用されるかが決定されます。それでもあいまいさが解消されない場合、すべてが保存され、エラボレータはそれらすべてを試行し、ちょうど1つがエラボレートできたときに成功することが期待されます。
+演算子と同様に、 {tech}[ローカル最長一致規則] が記法をパースする際に使用されます。もし複数の記法が最長一致で並んだ場合、宣言された優先順位によってどのパース結果が適用されるかが決定されます。それでもあいまいさが解消されない場合、すべてが保存され、エラボレータはそれらすべてを試行し、ちょうど1つがエラボレートできたときに成功することが期待されます。
 
 :::comment
 Rather than a single operator with its fixity and token, the body of a notation declaration consists of a sequence of {deftech}_notation items_, which may be either new {tech}[atoms] (including both keywords such as `if`, `#eval`, or `where` and symbols such as `=>`, `+`, `↗`, `⟦`, or `⋉`) or positions for terms.