HepLean Documentation

Lean.Util.OccursCheck

source
def Lean.occursCheck {m : Type → Type} [Monad m] [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 assignments and delayed assignments.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    partial def Lean.occursCheck.visitMVar {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (mvarId' : Lean.MVarId) :
    ExceptT Unit (StateT Lean.ExprSet m) Unit
    source
    partial def Lean.occursCheck.visit {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (e : Lean.Expr) :
    ExceptT Unit (StateT Lean.ExprSet m) Unit