Runs a term elaborator inside a tactic.

This function ensures that term elaboration fails when backtracking,
i.e., in `first| tac term | other`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- Lean.Elab.Tactic.runTermElab.go k mayPostpone = SeqLeft.seqLeft k fun (x : Unit) => Lean.Elab.Term.synthesizeSyntheticMVars (Lean.Elab.Term.PostponeBehavior.ofBool mayPostpone)

## Instances For

Elaborate `stx`

in the current `MVarContext`

. If given, the `expectedType`

will be used to help
elaboration but not enforced (use `elabTermEnsuringType`

to enforce an expected type).

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Elaborate `stx`

in the current `MVarContext`

. If given, the `expectedType`

will be used to help
elaboration and then a `TypeMismatchError`

will be thrown if the elaborated type doesn't match.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Try to close main goal using `x target`

, where `target`

is the type of the main goal.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- Lean.Elab.Tactic.sortMVarIdsByIndex mvarIds = do let __do_lift ← Lean.Elab.Tactic.sortMVarIdArrayByIndex (List.toArray mvarIds) pure __do_lift.toList

## Instances For

Execute `k`

, and collect new "holes" in the resulting expression.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Elaborates `stx`

and collects the `MVarId`

s of any holes that were created during elaboration.

With `allowNaturalHoles := false`

(the default), any new natural holes (`_`

) which cannot
be synthesized during elaboration cause `elabTermWithHoles`

to fail. (Natural goals appearing in
`stx`

which were created prior to elaboration are permitted.)

Unnamed `MVarId`

s are renamed to share the main goal's tag. If multiple unnamed goals are
encountered, `tagSuffix`

is appended to the main goal's tag along with a numerical index.

Note:

- Previously-created
`MVarId`

s which appear in`stx`

are not returned. - All parts of
`elabTermWithHoles`

operate at the current`MCtxDepth`

, and therefore may assign metavariables. - When
`allowNaturalHoles := true`

,`stx`

is elaborated under`withAssignableSyntheticOpaque`

, meaning that`.syntheticOpaque`

metavariables might be assigned during elaboration. This is a consequence of the implementation.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

If `allowNaturalHoles == true`

, then we allow the resultant expression to contain unassigned "natural" metavariables.
Recall that "natutal" metavariables are created for explicit holes `_`

and implicit arguments. They are meant to be
filled by typing constraints.
"Synthetic" metavariables are meant to be filled by tactics and are usually created using the synthetic hole notation `?<hole-name>`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Given a tactic

```
apply f
```

we want the `apply`

tactic to create all metavariables. The following
definition will return `@f`

for `f`

. That is, it will **not** create
metavariables for implicit arguments.
A similar method is also used in Lean 3.
This method is useful when applying lemmas such as:

```
theorem infLeRight {s t : Set α} : s ⊓ t ≤ t
```

where `s ≤ t`

here is defined as

```
∀ {x : α}, x ∈ s → x ∈ t
```

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

## Instances For

Elaborate `stx`

. If it is a free variable, return it. Otherwise, assert it, and return the free variable.
Note that, the main goal is updated when `Meta.assert`

is used in the second case.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.