diff --git a/LeanByExample/Type/Syntax.lean b/LeanByExample/Type/Syntax.lean index e9af1339..4ddda95a 100644 --- a/LeanByExample/Type/Syntax.lean +++ b/LeanByExample/Type/Syntax.lean @@ -4,7 +4,7 @@ 具象構文木とは何かを理解するには、私たちがエディタに `#eval "Hello"` などと入力したとき、Lean がこれを実行する過程で何をしているかを考えるとわかりやすいでしょう。入力された `#eval "Hello"` は最初は単なる文字列ですが、Lean はまずこれを Lean の文法に照らして合法的なコードであるか解析します。合法ならば次のステップに進むことができますし、そうでなければ「こんなコマンドは知らない」というエラーを表示します。この解析結果を保存する中間的データが具象構文木(`Syntax`)として表現されます。 -なお、ただの文字列を解析して構文木を得ることを構文解析またはパース(parse)と呼びます。 +なお、ただの文字列を解析して構文木を得ることを構文解析または **パース(parse)** と呼びます。 ## 定義