Documentation

Lean.Meta.CollectFVars

source
def Lean.Expr.collectFVars (e : Lean.Expr) :
StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
Instances For
    source
    def Lean.LocalDecl.collectFVars (localDecl : Lean.LocalDecl) :
    StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
    Instances For
      source
      def Lean.CollectFVars.State.addDependencies (s : Lean.CollectFVars.State) :
      Lean.MetaM Lean.CollectFVars.State

      For each variable in s.fvarSet, include its dependencies.

      Equations
      Instances For
        source
        def Lean.CollectFVars.State.addDependencies.getNext? :
        StateRefT' IO.RealWorld Nat (StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM) (Option Lean.FVarId)
        Instances For
          source
          partial def Lean.CollectFVars.State.addDependencies.go :
          StateRefT' IO.RealWorld Nat (StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM) Unit
          source
          def Lean.Meta.removeUnused (vars : Array Lean.Expr) (used : Lean.CollectFVars.State) :
          Lean.MetaM (Lean.LocalContext × Lean.LocalInstances × Array Lean.Expr)
          Instances For