diff --git a/doc/syntax.md b/doc/syntax.md index d1f8d2fc5c..df0ec10986 100644 --- a/doc/syntax.md +++ b/doc/syntax.md @@ -24,7 +24,7 @@ both programmers and proof engineers alike. 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. +continuation](https://youtu.be/vy4JWIiiXSY) 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).