Documentation

Lean.Util.FindMVar

source
@[reducible, inline]
abbrev Lean.FindMVar.Visitor :
Type
Equations
    Instances For
      source
      partial def Lean.FindMVar.visit (p : MVarId → Bool) (e : Expr) :
      Visitor
      source
      partial def Lean.FindMVar.main (p : MVarId → Bool) :
      Expr → Visitor
      source
      @[inline]
      def Lean.Expr.findMVar? (e : Expr) (p : MVarId → Bool) :
      Option MVarId
      Equations
        Instances For