def Lean.Meta.findLocalDeclWithType? (type : Expr) : MetaM (Option FVarId)

Return a local declaration whose type is definitionally equal to type.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MVarId.assumptionCore (mvarId : MVarId) : MetaM Bool

Return true if managed to close goal mvarId using an assumption.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MVarId.assumption (mvarId : MVarId) : MetaM Unit

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