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]