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 assignments and delayed assignments.

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