Documentation

Lean.Util.FindMVar

source
@[reducible, inline]
abbrev Lean.FindMVar.Visitor :
Type
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
    Instances For