Documentation

Lean.Util.FindMVar

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