feat(library/init): add helper functions

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'

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 :=

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

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"