HepLean Documentation

Batteries.Tactic.Exact

exact tactic (MetaM version) #

source
def Lean.MVarId.assignIfDefeq (g : Lean.MVarId) (e : Lean.Expr) :
Lean.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