Return a local declaration whose type is definitionally equal to type.
Instances For
Return true if managed to close goal mvarId using an assumption.
Instances For
@[deprecated Lean.MVarId.assumptionCore]
Instances For
Close goal mvarId using an assumption. Throw error message if failed.
Instances For
@[deprecated Lean.MVarId.assumption]