Documentation

Lean.Util.OccursCheck

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

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

Instances For