Documentation

Batteries.Tactic.Exact

exact tactic (MetaM version) #

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