Documentation

Lean.Meta.Tactic.Cleanup

source
def Lean.Meta.cleanup (mvarId : Lean.MVarId) :
Lean.MetaM Lean.MVarId

Auxiliary tactic for cleaning the local context. It removes local declarations (aka hypotheses) that are not relevant. We say a variable x is "relevant" if

  • It occurs in the target type, or
  • There is a relevant variable y that depends on x, or
  • The type of x is a proposition and it depends on a relevant variable y.
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.cleanup.addUsedFVars (e : Lean.Expr) :
StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
source
partial def Lean.Meta.cleanup.addDeps (fvarId : Lean.FVarId) :
StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
source
partial def Lean.Meta.cleanup.addUsedFVar (fvarId : Lean.FVarId) :
StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
source
def Lean.Meta.cleanup.collectPropsStep:
StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.cleanup.collectProps:
StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
source
def Lean.Meta.cleanup.collectUsed (mvarId : Lean.MVarId) :
StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Lean.FVarIdSet
Equations
  • One or more equations did not get rendered due to their size.