diff --git a/doc/syntax.md b/doc/syntax.md index 7858e8ab72..a9f1632409 100644 --- a/doc/syntax.md +++ b/doc/syntax.md @@ -66,5 +66,6 @@ The new notation is preferred to the binary notation since the latter, before ch If there are multiple notations accepting the same longest parse, the choice will be delayed until elaboration, which will fail unless exactly one overload is type correct. ## Syntax and Macros - ## Elaborators + +TODO. See [Lean Together 2021: Metaprogramming in Lean 4](https://youtu.be/hxQ1vvhYN_U) for an overview as well [the continuation](https://youtu.be/hxQ1vvhYN_U) about tactic programming. For more information on antiquotations, see also ยง4.1 of [Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages](https://arxiv.org/pdf/2001.10490.pdf#page=11).