From 2f6f1eb458ea1436a1986033a3acde699c46129a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Feb 2017 16:23:15 -0800
Subject: [PATCH] feat(library/init): add helper functions

---
 library/init/category/combinators.lean | 3 +++
 library/init/meta/environment.lean     | 6 ++++++
 library/init/meta/expr.lean            | 3 +++
 library/init/meta/tactic.lean          | 1 -
 4 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/library/init/category/combinators.lean b/library/init/category/combinators.lean
index ef2e2684b1..d034302bc0 100644
--- a/library/init/category/combinators.lean
+++ b/library/init/category/combinators.lean
@@ -48,6 +48,9 @@ ite c t (pure ())
 def mcond {m : Type → Type} [monad m] {α : Type} (mbool : m bool) (tm fm : m α) : m α :=
 do b ← mbool, cond b tm fm
 
+def mwhen {m : Type → Type} [monad m] (c : m bool) (t : m unit) : m unit :=
+mcond c t (return ())
+
 namespace monad
 def mapm   := @mmap
 def mapm'  := @mmap'
diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean
index d0745feac4..733812ab51 100644
--- a/library/init/meta/environment.lean
+++ b/library/init/meta/environment.lean
@@ -98,6 +98,12 @@ end
 meta def in_current_file (env : environment) (n : name) : bool :=
 (env^.decl_olean n)^.is_none && env^.contains n
 
+meta def is_definition (env : environment) (n : name) : bool :=
+match env^.get n with
+| exceptional.success (declaration.defn _ _ _ _ _ _) := tt
+| _                                                  := ff
+end
+
 end environment
 
 meta instance : has_to_string environment :=
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index 87f4d86cd2..8ad2753508 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -323,4 +323,7 @@ meta def to_raw_fmt : expr → format
 | (elet n g e f) := p ["elet", to_fmt n, to_raw_fmt g, to_raw_fmt e, to_raw_fmt f]
 | (macro d n args) := sbracket (format.join (list.intersperse " " ("macro" :: to_fmt (macro_def_name d) :: list.map to_raw_fmt (macro_args_to_list n args))))
 
+meta def mfold {α : Type} {m : Type → Type} [monad m] (e : expr) (a : α) (fn : expr → nat → α → m α) : m α :=
+fold e (return a) (λ e n a, a >>= fn e n)
+
 end expr
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 39ad994dbe..070eae4d83 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -168,7 +168,6 @@ meta instance (α : Type u) (β : Type v) [has_to_tactic_format α] [has_to_tact
  has_to_tactic_format (α × β) :=
 ⟨λ ⟨a, b⟩, to_fmt <$> (prod.mk <$> pp a <*> pp b)⟩
 
-
 meta def option_to_tactic_format {α : Type u} [has_to_tactic_format α] : option α → tactic format
 | (some a) := do fa ← pp a, return (to_fmt "(some " ++ fa ++ ")")
 | none     := return "none"