Documentation

Batteries.Tactic.Exact

exact tactic (MetaM version) #

source
def Lean.MVarId.assignIfDefEq (g : MVarId) (e : Expr) :
MetaM Unit

MetaM version of Lean.Elab.Tactic.evalExact: add mvarId := x to the metavariable assignment. This method wraps Lean.MVarId.assign, checking whether mvarId is already assigned, and whether the expression has the right type.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[deprecated Lean.MVarId.assignIfDefEq (since := "2025-04-09")]
    def Lean.MVarId.assignIfDefeq (g : MVarId) (e : Expr) :
    MetaM Unit

    Alias of Lean.MVarId.assignIfDefEq.

    MetaM version of Lean.Elab.Tactic.evalExact: add mvarId := x to the metavariable assignment. This method wraps Lean.MVarId.assign, checking whether mvarId is already assigned, and whether the expression has the right type.

    Equations
    Instances For