Skip to content

Commit

Permalink
Macro の説明文の校正
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Jan 12, 2025
1 parent 9658d00 commit 4804f3f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion LeanByExample/Type/Macro.lean
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/- # Macro
`Lean.Macro` 型の項は、マクロを表現しています。一般のプログラミング言語においてマクロとは構文を構文に変換することですが、Lean の `m : Macro` は、`Syntax → MacroM Syntax` という型の関数そのものです。
`Lean.Macro` 型の項は、マクロを表現しています。一般のプログラミング言語においてマクロとは構文を構文に変換することを指す言葉で、必ずしも特定の型や項に対応する概念ではありませんが、Lean の `m : Macro` は、`Syntax → MacroM Syntax` という型の関数そのものです。
[`Syntax`](./Syntax.md) 型が Lean の構文木をダイレクトに表していたように、`Macro` 型は Lean のマクロをダイレクトに表しています。
-/
Expand Down

0 comments on commit 4804f3f

Please sign in to comment.