Documentation

Lean.Util.CollectMVars

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