How does the attribute actually works?

Stream: lean4

[Lim, Thing-han]

I know that attribute such as, builtinTermElab, somehow registers a term elaboration rule.
But for example,
@[builtinTermElab «hole»] def elabHole : Syntax → Option Expr → TermElabM Expr

How does «hole» know what to use as an expected type (argument of type Option Expr) ?