Return a local declaration whose type is definitionally equal to type
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return true
if managed to close goal mvarId
using an assumption.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[deprecated Lean.MVarId.assumptionCore]
Equations
- Lean.Meta.assumptionCore mvarId = mvarId.assumptionCore
Instances For
Close goal mvarId
using an assumption. Throw error message if failed.
Equations
- mvarId.assumption = do let __do_lift ← mvarId.assumptionCore if __do_lift = true then pure PUnit.unit else Lean.Meta.throwTacticEx `assumption mvarId
Instances For
@[deprecated Lean.MVarId.assumption]
Equations
- Lean.Meta.assumption mvarId = mvarId.assumption