Documentation

Lean.Util.CollectMVars

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