max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: link to some macro documentation

Browse source
This commit is contained in:
Sebastian Ullrich 2021-08-08 12:41:59 +02:00
parent 358a129d78
commit 341b4ac652
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
doc/syntax.md
View file

@ -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).