Zulip Chat Archive

Stream: lean4

Topic: How does the attribute actually works?

view this post on Zulip Lim, Thing-han (Mar 12 2021 at 16:02):

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) ?

Last updated: May 18 2021 at 23:14 UTC