Macros

<< Steps to metal

Which goes, From input state

let a := 2

|> 1. Parsing

Lean Syntax object or commonly known as Concrete Syntax Tree

|> 2. Elaboration

Lean Expr object or commonly known as Abstract Syntax Tree

|> 3. Evaluation

C string or int a = 2;

|> 4. C Compiler

Binary string 0100100

The steps above restate what's written in the image. It's to make them readable.

<< So where are the macros?

Macros, according to the book is just "glorified regular expression" I think what the book is trying to convey is the way in which Syntax objects are created and probably how they are parsed.