def
Lean.occursCheck
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadMCtx m]
(mvarId : Lean.MVarId)
(e : Lean.Expr)
:
m Bool
Return true if e does 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.occursCheck.visitMVar
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadMCtx m]
(mvarId : Lean.MVarId)
(mvarId' : Lean.MVarId)
:
partial def
Lean.occursCheck.visit
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadMCtx m]
(mvarId : Lean.MVarId)
(e : Lean.Expr)
: