# `elabTerm` for Tactics and basic tactics that use it. #

source
def Lean.Elab.Tactic.runTermElab {α : Type} (k : TermElabM α) (mayPostpone : Bool := false) :
TacticM α

Runs a term elaborator inside a tactic, finalizing elaboration with `Term.synthesizeSyntheticMVars`.

- `mayPostpone` controls the postponement behavior of `Term.synthesizeSyntheticMVars`.

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

source
def Lean.Elab.Tactic.elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone : Bool := false) :
TacticM Expr

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

source
def Lean.Elab.Tactic.elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpone : Bool := false) :
TacticM Expr

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

source
def Lean.Elab.Tactic.logUnassignedAndAbort (mvarIds : Array MVarId) :
TacticM Unit
Equations

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

Instances For

source
def Lean.Elab.Tactic.filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) :
MetaM (Array MVarId)
Equations

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

Instances For

source
def Lean.Elab.Tactic.closeMainGoalUsing (tacName : Name) (x : Expr → Name → TacticM Expr) (checkNewUnassigned : Bool := true) :
TacticM Unit

Try to close main goal using `x target tag`, where `target` is the type of the main goal and `tag` is its user name.

If `checkNewUnassigned` is true, then throws an error if the resulting value has metavariables that were created during the execution of `x`. If it is false, then it is the responsibility of `x` to add such metavariables to the goal list.

During the execution of `x`:

- The local context is that of the main goal.
- The goal list has the main goal removed.
- It is allowable to modify the goal list, for example with `Lean.Elab.Tactic.pushGoals`.

On failure, the main goal remains at the front of the goal list.

Equations

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

Instances For

source
def Lean.Elab.Tactic.evalExact :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.sortMVarIdArrayByIndex {m : Type → Type} [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) :
m (Array MVarId)
Equations

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

Instances For

source
def Lean.Elab.Tactic.sortMVarIdsByIndex {m : Type → Type} [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) :
m (Array MVarId)
Equations

- Lean.Elab.Tactic.sortMVarIdsByIndex mvarIds = do let __do_lift ← Lean.Elab.Tactic.sortMVarIdArrayByIndex mvarIds pure __do_lift

Instances For

source
def Lean.Elab.Tactic.collectFreshMVars {m : Type → Type u_1} [Monad m] [MonadLiftT MetaM m] (k : m Expr) :
m (Expr × Array MVarId)

Execute `k`, and collect any fresh metavariables created during the execution of `k`.

Equations

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

Instances For

source
def Lean.Elab.Tactic.withCollectingNewGoalsFrom (k : TacticM Expr) (parentTag tagSuffix : Name) (allowNaturalHoles : Bool := false) :
TacticM (Expr × List MVarId)

Execute `k`, and collect new "holes" in the resulting expression.

- `parentTag` and `tagSuffix` are used to tag untagged goals with `Lean.Elab.Tactic.tagUntaggedGoals`.
- If `allowNaturalHoles` is true, then `_`'s are allowed and create new goals.

Equations

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

Instances For

source
def Lean.Elab.Tactic.elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles : Bool := false) (parentTag? : Option Name := none) :
TacticM (Expr × List MVarId)

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 tag `parentTag?` (or the main goal's tag if `parentTag?` is `none`). If multiple unnamed goals are encountered, `tagSuffix` is appended to this 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

source
def Lean.Elab.Tactic.refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) :
TacticM Unit

If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables. Recall that "natural" 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

source
def Lean.Elab.Tactic.evalRefine :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.evalRefine' :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.evalSpecialize :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.elabTermForApply (stx : Syntax) (mayPostpone : Bool := true) :
TacticM Expr

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

source
def Lean.Elab.Tactic.getFVarId (id : Syntax) :
TacticM FVarId
Equations

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

Instances For

source
def Lean.Elab.Tactic.getFVarIds (ids : Array Syntax) :
TacticM (Array FVarId)
Equations

- Lean.Elab.Tactic.getFVarIds ids = Lean.Elab.Tactic.withMainContext (Array.mapM Lean.Elab.Tactic.getFVarId ids)

Instances For

source
def Lean.Elab.Tactic.evalApplyLikeTactic (tac : MVarId → Expr → MetaM (List MVarId)) (e : Syntax) :
TacticM Unit
Equations

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

Instances For

source
def Lean.Elab.Tactic.evalApply :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.evalConstructor :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.evalWithReducible :
Tactic
Equations

- Lean.Elab.Tactic.evalWithReducible stx = Lean.Meta.withReducible (Lean.Elab.Tactic.evalTactic stx[1])

Instances For

source
def Lean.Elab.Tactic.evalWithReducibleAndInstances :
Tactic
Equations

- Lean.Elab.Tactic.evalWithReducibleAndInstances stx = Lean.Meta.withReducibleAndInstances (Lean.Elab.Tactic.evalTactic stx[1])

Instances For

source
def Lean.Elab.Tactic.evalWithUnfoldingAll :
Tactic
Equations

- Lean.Elab.Tactic.evalWithUnfoldingAll stx = Lean.Meta.withTransparency Lean.Meta.TransparencyMode.all (Lean.Elab.Tactic.evalTactic stx[1])

Instances For

source
def Lean.Elab.Tactic.elabAsFVar (stx : Syntax) (userName? : Option Name := none) :
TacticM FVarId

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

source
def Lean.Elab.Tactic.evalRename :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) :
TacticM Unit
Equations

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

Instances For

source
def Lean.Elab.Tactic.elabDecideConfig :
Syntax → TacticM Parser.Tactic.DecideConfig
Equations

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

Instances For

source
def Lean.Elab.Tactic.evalDecide :
Tactic
Equations

- Lean.Elab.Tactic.evalDecide stx = do let cfg ← Lean.Elab.Tactic.elabDecideConfig stx[1] Lean.Elab.Tactic.evalDecideCore `decide cfg

Instances For

source
def Lean.Elab.Tactic.evalNativeDecide :
Tactic
Equations

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

Instances For