def Lean.Meta.findLocalDeclWithType? (type : Lean.Expr) : Lean.MetaM (Option Lean.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 : Lean.MVarId) : Lean.MetaM Bool

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

def Lean.MVarId.assumption (mvarId : Lean.MVarId) : Lean.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