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
«hole» know what to use as an expected type (argument of type
Option Expr) ?
Last updated: May 18 2021 at 23:14 UTC