#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen
Type Theory Forall
00:00
Exploring Macros, Quotation, and Syntax in Lean
The chapter dives deep into the intricacies of macros and quotation in systems like Lean, emphasizing the significance of hygiene in macros and elaborators. It discusses the flexibility and power of Lean Macros, handling syntax to syntax translation, as well as the challenges of variable capture when working with Lean code. The conversation touches on extending concrete syntax, syntax macros, quasi-quotation, and the differences in compile time information handling between Lean and Racket.
Transcript
Play full episode
