elabTerm for Tactics and basic tactics that use it.

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

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.

def Lean.Elab.Tactic.runTermElab.go {α : Type} (k : Lean.Elab.TermElabM α) (mayPostpone : optParam Bool false) : Lean.Elab.TermElabM α

Equations

• Lean.Elab.Tactic.runTermElab.go k mayPostpone = SeqLeft.seqLeft k fun x => Lean.Elab.Term.synthesizeSyntheticMVars mayPostpone false

def Lean.Elab.Tactic.elabTerm (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (mayPostpone : optParam Bool false) : Lean.Elab.Tactic.TacticM Lean.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.

def Lean.Elab.Tactic.elabTermEnsuringType (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (mayPostpone : optParam Bool false) : Lean.Elab.Tactic.TacticM Lean.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.

def Lean.Elab.Tactic.closeMainGoalUsing (x : Lean.Expr → Lean.Elab.Tactic.TacticM Lean.Expr) (checkUnassigned : optParam Bool true) : Lean.Elab.Tactic.TacticM Unit

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.

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.evalExact : Lean.Elab.Tactic.Tactic

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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 ?.

Equations

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

def Lean.Elab.Tactic.evalRefine : Lean.Elab.Tactic.Tactic

Equations

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

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

Equations

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

def Lean.Elab.Tactic.evalSpecialize : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.elabTermForApply (stx : Lean.Syntax) (mayPostpone : optParam Bool true) : Lean.Elab.Tactic.TacticM Lean.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
⊓ t ≤ t
≤ t

where s ≤ t≤ t here is defined as

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.evalApply : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalConstructor : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalWithReducible : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalWithReducibleAndInstances : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalWithUnfoldingAll : Lean.Elab.Tactic.Tactic

Equations

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

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

Elaborate stx. If it 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.

def Lean.Elab.Tactic.evalRename : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalDecide : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalNativeDecide : Lean.Elab.Tactic.Tactic

Equations

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