the method resolveName adds a completion point for it using the given
expected type. Thus, we propagate the expected type if stx[0] is an identifier.
It doesn't "hurt" if the identifier can be resolved because the expected type is not used in this case.
Recall that if the name resolution fails a synthetic sorry is returned.
Returns true if stx is a by expression with an empty tactic body
(not a parse error producing .missing).
The structure is: node byTactic [atom "by", node tacticSeq [node tacticSeq1Indented [node null []]]]
Instances For
Returns true if all conditions are met for empty by to be elaborated as try?:
the body is empty, the option is enabled, we are in an interactive (non-combinator) context,
and the try? infrastructure (parser Lean.Parser.Tactic.tryTrace) is available — the latter
matters when working on the prelude, before Init.Try is imported.
Instances For
Body of the byTactic term elaborator: registers a tactic mvar for the body, or
errors when there's no expected type. Shared between elabByTactic and
Lean.Elab.Tactic.Try's elabEmptyByAsTry so the two paths can't drift.