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.

partial def Lean.occursCheck.visitMVar {m : Type → Type} [Monad m] [MonadMCtx m] (mvarId mvarId' : MVarId) : ExceptT Unit (StateT ExprSet m) Unit

partial def Lean.occursCheck.visit {m : Type → Type} [Monad m] [MonadMCtx m] (mvarId : MVarId) (e : Expr) : ExceptT Unit (StateT ExprSet m) Unit