Documentation

Lean.Util.FindMVar

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