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