From 03fb5916046fb803a2f1df4dfc20e8a94146d37b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Jan 2020 15:49:13 -0800
Subject: [PATCH] feat: add `findMVar?`

---
 src/Init/Lean/Util/FindMVar.lean | 33 ++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 src/Init/Lean/Util/FindMVar.lean

diff --git a/src/Init/Lean/Util/FindMVar.lean b/src/Init/Lean/Util/FindMVar.lean
new file mode 100644
index 0000000000..e685d76969
--- /dev/null
+++ b/src/Init/Lean/Util/FindMVar.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Expr
+
+namespace Lean
+
+namespace FindMVar
+
+abbrev Visitor := Option MVarId → Option MVarId
+
+@[inline] def visit (f : Expr → Visitor) (e : Expr) : Visitor :=
+fun s => if s.isSome || !e.hasMVar then s else f e s
+
+@[specialize] partial def main (p : MVarId → Bool) : Expr → Visitor
+| Expr.proj _ _ e _    => visit main e
+| Expr.forallE _ d b _ => visit main b ∘ visit main d
+| Expr.lam _ d b _     => visit main b ∘ visit main d
+| Expr.letE _ t v b _  => visit main b ∘ visit main v ∘ visit main t
+| Expr.app f a _       => visit main a ∘ visit main f
+| Expr.mdata _ b _     => visit main b
+| Expr.mvar mvarId _   => fun s => if s.isNone && p mvarId then some mvarId else s
+| _                    => id
+
+end FindMVar
+
+@[inline] def Expr.findMVar? (e : Expr) (p : MVarId → Bool) : Option MVarId :=
+FindMVar.main p e none
+
+end Lean