def Lean.occursCheck {m : Type → Type} [Monad m] [MonadMCtx m] (mvarId : MVarId) (e : Expr) : m Bool

Return true if e does not contain mvarId directly or indirectly This function considers assignments and delayed assignments.

Equations

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