Documentation

Lean.Util.CollectFVars

source
structure Lean.CollectFVars.State :
Type
Instances For
    source
    instance Lean.CollectFVars.instInhabitedState :
    Inhabited State
    Equations
      source
      def Lean.CollectFVars.State.add (s : State) (fvarId : FVarId) :
      State
      Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Lean.CollectFVars.Visitor :
          Type
          Equations
            Instances For
              source
              partial def Lean.CollectFVars.visit (e : Expr) :
              Visitor
              source
              partial def Lean.CollectFVars.main :
              Expr → Visitor
              source
              def Lean.collectFVars (s : CollectFVars.State) (e : Expr) :
              CollectFVars.State
              Equations
                Instances For