Documentation

Lean.Util.CollectFVars

source
structure Lean.CollectFVars.State :
Type
Instances For
    source
    def Lean.CollectFVars.instInhabitedState.default :
    State
    Instances For
      source
      @[implicit_reducible]
      instance Lean.CollectFVars.instInhabitedState :
      Inhabited State
      source
      def Lean.CollectFVars.State.add (s : State) (fvarId : FVarId) :
      State
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.CollectFVars.Visitor :
        Type
        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
          Instances For