def Lean.Elab.Term.annotateFirstHoleWithType (t : Lean.Term) (type : Lean.Expr) :
Adds a type annotation to a hole that occurs immediately at the beginning of the term. This is so that coercions can trigger when elaborating the term. See https://github.com/leanprover/lean4/issues/2040 for futher rationale.
_ < 3is annotated
(_) < 3is not, because it occurs after an atom
_ < _only the first one is annotated
_ + 2 < 3is annotated (not the best heuristic, ideally we'd like to annotate
_ + 2)
lt _ 3is not, because it occurs after an identifier