diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 632940ac85..1229c10312 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -161,6 +161,10 @@ do t ← target,
    | _                 := return []
    end
 
+meta_definition note (n : name) (pr : expr) : tactic unit :=
+do t ← infer_type pr,
+   pose n t pr
+
 meta_definition intro_lst : list name → tactic (list expr)
 | []      := return []
 | (n::ns) := do H ← intro n, Hs ← intro_lst ns, return (H :: Hs)