Documentation

Lean.Util.OccursCheck

source
def Lean.MetavarContext.occursCheck (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (e : Lean.Expr) :
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.
source
partial def Lean.MetavarContext.occursCheck.visitMVar (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (mvarId' : Lean.MVarId) :
EStateM Unit Lean.ExprSet Unit
source
partial def Lean.MetavarContext.occursCheck.visit (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (e : Lean.Expr) :
EStateM Unit Lean.ExprSet Unit