def Lean.mustNotOccursCheck (mvarId : MVarId) (e : Expr) : MetaM Bool

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

Equations

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

partial def Lean.mustNotOccursCheck.visitMVar (mvarId mvarId' : MVarId) : ExceptT Unit (StateT ExprSet MetaM) Unit

partial def Lean.mustNotOccursCheck.visit (mvarId : MVarId) (e : Expr) : ExceptT Unit (StateT ExprSet MetaM) Unit

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

Return true if e must contain mvarId as a subterm directly or indirectly after further mvar instantiation and β-reduction This function considers assigments and delayed assignments.

Equations

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

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

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