7.7. Custom Tactics🔗

Lean.Elab.Tactic.withLocation (loc : Location)
    (atLocal : Lean.FVarId → TacticM Unit)
    (atTarget : TacticM Unit)
    (failed : Lean.MVarId → TacticM Unit)
    : TacticM Unit

Runs the given atLocal and atTarget methods on each of the locations selected by the given loc.

• If loc is a list of locations, runs at each specified hypothesis (and finally the goal if ⊢ is included), and fails if any of the tactic applications fail.

• If loc is *, runs at the target first and then the hypotheses in reverse order. If atTarget closes the main goal, withLocation does not run atLocal. If all tactic applications fail, withLocation with call failed with the main goal mvar.

Lean.Elab.Tactic.getGoals
    : TacticM (List Lean.MVarId)

Returns the list of goals. Goals may or may not already be assigned.

Lean.Elab.Tactic.getMainGoal
    : TacticM Lean.MVarId

Return the first goal.

Lean.Elab.Tactic.getMainTag : TacticM Lean.Name

Return the main goal tag.

Lean.Elab.Tactic.closeMainGoal
  (tacName : Lean.Name) (val : Lean.Expr)
  (checkUnassigned : Bool := true) :
  TacticM Unit

Closes main goal using the given expression. If checkUnassigned == true, then val must not contain unassigned metavariables. Returns true if val was successfully used to close the goal.

Lean.Elab.Tactic.tagUntaggedGoals
    (parentTag newSuffix : Lean.Name)
    (newGoals : List Lean.MVarId) : TacticM Unit

Use parentTag to tag untagged goals at newGoals. If there are multiple new untagged goals, they are named using <parentTag>.<newSuffix>_<idx> where idx > 0. If there is only one new untagged goal, then we just use parentTag

Lean.Elab.Tactic.appendGoals
    (mvarIds : List Lean.MVarId) : TacticM Unit

Add the given goals at the end of the current list of goals.

Lean.Elab.Tactic.closeMainGoalUsing
  (tacName : Lean.Name)
  (x :
    Lean.Expr → Lean.Name → TacticM Lean.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.

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

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

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

Elaborates stx and collects the MVarIds 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 MVarIds 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 MVarIds 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.