search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
51 stars 7 forks source link

MacroM 型を紹介する #1105

Open Seasawher opened 1 week ago

Seasawher commented 1 week ago 
/--
The `MacroM` monad is the main monad for macro expansion. It has the
information needed to handle hygienic name generation, and is the monad that
`macro` definitions live in.

Notably, this is a (relatively) pure monad: there is no `IO` and no access to
the `Environment`. That means that things like declaration lookup are
impossible here, as well as `IO.Ref` or other side-effecting operations.
For more capabilities, macros can instead be written as `elab` using `adaptExpander`.
-/
abbrev MacroM := ReaderT Macro.Context (EStateM Macro.Exception Macro.State)