From 341b4ac652eb24471aeb55060f423fe6616025b2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 8 Aug 2021 12:41:59 +0200 Subject: [PATCH] doc: link to some macro documentation --- doc/syntax.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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).