Documentation

Lean.Meta.CollectFVars

source
def Lean.Expr.collectFVars (e : Expr) :
StateRefT' IO.RealWorld CollectFVars.State MetaM Unit
Equations
    Instances For
      source
      def Lean.LocalDecl.collectFVars (localDecl : LocalDecl) :
      StateRefT' IO.RealWorld CollectFVars.State MetaM Unit
      Equations
        Instances For
          source
          def Lean.CollectFVars.State.addDependencies (s : State) :
          MetaM 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 State MetaM) (Option FVarId)
              Equations
                Instances For
                  source
                  partial def Lean.CollectFVars.State.addDependencies.go :
                  StateRefT' IO.RealWorld Nat (StateRefT' IO.RealWorld State MetaM) Unit
                  source
                  def Lean.Meta.removeUnused (vars : Array Expr) (used : CollectFVars.State) :
                  MetaM (LocalContext × LocalInstances × Array Expr)
                  Equations
                    Instances For