Return a local declaration whose type is definitionally equal to type
.
Equations
- One or more equations did not get rendered due to their size.
Return true
if managed to close goal mvarId
using an assumption.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.assumptionCore mvarId = Lean.MVarId.assumptionCore mvarId
Close goal mvarId
using an assumption. Throw error message if failed.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.assumption mvarId = Lean.MVarId.assumption mvarId