diff --git a/library/data/list.lean b/library/data/list.lean
index 460f9fe6dc..dd9c9f3c64 100644
--- a/library/data/list.lean
+++ b/library/data/list.lean
@@ -5,7 +5,6 @@ Author: Jeremy Avigad
 
 This is a minimal port of functions from the lean2 list library.
 -/
-
 import init.list
 import algebra.order
 import data.nat
diff --git a/tmp/cli_debugger.lean b/library/debugger/cli.lean
similarity index 61%
rename from tmp/cli_debugger.lean
rename to library/debugger/cli.lean
index ffddb96383..cc0bf1e781 100644
--- a/tmp/cli_debugger.lean
+++ b/library/debugger/cli.lean
@@ -1,3 +1,12 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Simple command line interface for debugging Lean programs and tactics.
+-/
+import debugger.util
+
 namespace debugger
 
 inductive mode
@@ -16,66 +25,12 @@ def init_state : state :=
 { md := mode.init, csz := 0,
   fn_bps := [], active_bps := [] }
 
-def is_space (c : char) : bool :=
-if c = ' ' ∨ c = char.of_nat 11 ∨ c = '\n' then tt else ff
-
-def split_core : string → string → list string
-| (c::cs) [] :=
-  if is_space c then split_core cs [] else split_core cs [c]
-| (c::cs) r  :=
-  if is_space c then r^.reverse :: split_core cs [] else split_core cs (c::r)
-| []      [] := []
-| []      r  := [r^.reverse]
-
-def split (s : string) : list string :=
-(split_core s [])^.reverse
-
-def to_qualified_name_core : string → string → name
-| []      r := if r = [] then name.anonymous else mk_simple_name r^.reverse
-| (c::cs) r :=
-  if is_space c then to_qualified_name_core cs r
-  else if c = '.' then
-       if r = [] then to_qualified_name_core cs []
-       else           name.mk_string r^.reverse (to_qualified_name_core cs [])
-  else to_qualified_name_core cs (c::r)
-
-def to_qualified_name (s : string) : name :=
-to_qualified_name_core s []
-
-meta def get_file (fn : name) : vm string :=
-do {
-  d ← vm.get_decl fn,
-  some n ← return (vm_decl.olean d) | failure,
-  return n
-}
-<|>
-return "[current file]"
-
-meta def pos_info (fn : name) : vm string :=
-do {
-  d                ← vm.get_decl fn,
-  some (line, col) ← return (vm_decl.pos d) | failure,
-  file             ← get_file fn,
-  return (file ++ ":" ++ line^.to_string ++ ":" ++ col^.to_string)
-}
-<|>
-return "<position not available>"
-
-meta def show_fn (header : string) (fn : name) (frame : nat) : vm unit :=
-do pos ← pos_info fn,
-   vm.put_str ("[" ++ frame^.to_string ++ "] " ++ header ++ " " ++ fn^.to_string ++ " at " ++ pos ++ "\n")
-
-meta def show_curr_fn (header : string) : vm unit :=
-do fn ← vm.curr_fn,
-   sz ← vm.call_stack_size,
-   show_fn header fn (sz-1)
-
 meta def show_help : vm unit :=
 do
- vm.put_str "exit      - stop debugger\n",
- vm.put_str "help      - display this message\n",
- vm.put_str "run       - continue execution\n",
- vm.put_str "step      - execute until another function in on the top of the stack\n",
+ vm.put_str "exit       - stop debugger\n",
+ vm.put_str "help       - display this message\n",
+ vm.put_str "run        - continue execution\n",
+ vm.put_str "step       - execute until another function in on the top of the stack\n",
  vm.put_str "stack trace\n",
  vm.put_str " up        - move up in the stack trace\n",
  vm.put_str " down      - move down in the stack trace\n",
@@ -88,13 +43,6 @@ do
  vm.put_str " rbreak fn - remove breakpoint\n",
  vm.put_str " bs        - show breakpoints\n"
 
-meta def is_valid_fn_prefix (p : name) : vm bool :=
-do env ← vm.get_env,
-   return $ env^.fold ff (λ d r,
-     r ||
-     let n := d^.to_name in
-     p^.is_prefix_of n)
-
 meta def add_breakpoint (s : state) (args : list string) : vm state :=
 match args with
 | [arg] := do
@@ -128,67 +76,15 @@ meta def show_breakpoints : list name → vm unit
   vm.put_str "\n",
   show_breakpoints fns
 
-meta def show_frame (frame : nat) : vm unit :=
-do sz ← vm.call_stack_size,
-   fn ← if frame >= sz then vm.curr_fn else vm.call_stack_fn frame,
-   show_fn "frame" fn frame
-
-meta def up (frame : nat) : vm nat :=
+meta def up_cmd (frame : nat) : vm nat :=
 if frame = 0 then return 0
 else show_frame (frame - 1) >> return (frame - 1)
 
-meta def down (frame : nat) : vm nat :=
+meta def down_cmd (frame : nat) : vm nat :=
 do sz ← vm.call_stack_size,
    if frame >= sz - 1 then return frame
    else show_frame (frame + 1) >> return (frame + 1)
 
-meta def type_to_string : option expr → nat → vm string
-| none i := do
-  o ← vm.stack_obj i,
-  match o^.kind with
-  | vm_obj_kind.simple       := return "[tagged value]"
-  | vm_obj_kind.constructor  := return "[constructor]"
-  | vm_obj_kind.closure      := return "[closure]"
-  | vm_obj_kind.mpz          := return "[big num]"
-  | vm_obj_kind.name         := return "name"
-  | vm_obj_kind.level        := return "level"
-  | vm_obj_kind.expr         := return "expr"
-  | vm_obj_kind.declaration  := return "declaration"
-  | vm_obj_kind.environment  := return "environment"
-  | vm_obj_kind.tactic_state := return "tactic_state"
-  | vm_obj_kind.format       := return "format"
-  | vm_obj_kind.options      := return "options"
-  | vm_obj_kind.other        := return "[other]"
-  end
-| (some type) i := do
-  fmt ← vm.pp_expr type,
-  opts ← vm.get_options,
-  return (fmt^.to_string opts)
-
-meta def show_vars_core : nat → nat → nat → vm unit
-| c i e :=
-  if i = e then return ()
-  else do
-    (n, type) ← vm.stack_obj_info i,
-    type_str  ← type_to_string type i,
-    vm.put_str $ "#" ++ c^.to_string ++ " " ++ n^.to_string ++ " : " ++ type_str ++ "\n",
-    show_vars_core (c+1) (i+1) e
-
-meta def show_vars (frame : nat) : vm unit :=
-do (s, e) ← vm.call_stack_var_range frame,
-   show_vars_core 0 s e
-
-meta def show_stack_core : nat → vm unit
-| 0     := return ()
-| (i+1) := do
-  fn ← vm.call_stack_fn i,
-  show_fn "stack" fn i,
-  show_stack_core i
-
-meta def show_stack : vm unit :=
-do sz ← vm.call_stack_size,
-   show_stack_core sz
-
 meta def pidx_cmd : nat → list string → vm unit
 | frame [arg] := do
   idx     ← return $ arg^.to_nat,
@@ -243,18 +139,18 @@ meta def cmd_loop_core : state → nat → list string → vm state
     match tks with
     | []          := cmd_loop_core s frame default_cmd
     | (cmd::args) :=
-      if cmd = "help" then show_help >> cmd_loop_core s frame default_cmd
+      if cmd = "help" ∨ cmd = "h" then show_help >> cmd_loop_core s frame []
       else if cmd = "exit" then return {s with md := mode.done }
       else if cmd = "run" ∨ cmd = "r" then return {s with md := mode.run }
       else if cmd = "step" ∨ cmd = "s" then return {s with md := mode.step }
-      else if cmd = "break" ∨ cmd = "b" then do new_s ← add_breakpoint s args, cmd_loop_core new_s frame default_cmd
-      else if cmd = "rbreak" then do new_s ← remove_breakpoint s args, cmd_loop_core new_s frame default_cmd
+      else if cmd = "break" ∨ cmd = "b" then do new_s ← add_breakpoint s args, cmd_loop_core new_s frame []
+      else if cmd = "rbreak" then do new_s ← remove_breakpoint s args, cmd_loop_core new_s frame []
       else if cmd = "bs" then do
         vm.put_str "breakpoints\n",
         show_breakpoints s^.fn_bps,
         cmd_loop_core s frame default_cmd
-      else if cmd = "up" ∨ cmd = "u" then do frame ← up frame, cmd_loop_core s frame ["u"]
-      else if cmd = "down" ∨ cmd = "d" then do frame ← down frame, cmd_loop_core s frame ["d"]
+      else if cmd = "up" ∨ cmd = "u" then do frame ← up_cmd frame, cmd_loop_core s frame ["u"]
+      else if cmd = "down" ∨ cmd = "d" then do frame ← down_cmd frame, cmd_loop_core s frame ["d"]
       else if cmd = "vars" ∨ cmd = "v" then do show_vars frame, cmd_loop_core s frame []
       else if cmd = "stack" then do show_stack, cmd_loop_core s frame []
       else if cmd = "pidx" then do pidx_cmd frame args, cmd_loop_core s frame []
@@ -332,29 +228,6 @@ do s ← prune_active_bps s,
 
 meta def monitor : vm_monitor state :=
 { init := init_state, step := step_fn }
-
-def attr : user_attribute :=
-{ name  := `breakpoint,
-  descr := "breakpoint for debugger" }
-
 end debugger
 
 run_command vm_monitor.register `debugger.monitor
-run_command attribute.register `debugger.attr
-
-set_option debugger true
-set_option debugger.autorun true
-
-def g (c : nat) := c + 1
-
-def h (a : nat) (b : nat) := g (b+2) + a
-
-def s (a : nat) := h 2 a + h 3 a
-
-local attribute [breakpoint] h
-
-def f : nat → nat
-| 0     := s 0
-| (a+1) := f a
-
-vm_eval f 3
diff --git a/library/debugger/default.lean b/library/debugger/default.lean
new file mode 100644
index 0000000000..23cd7d0f01
--- /dev/null
+++ b/library/debugger/default.lean
@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import debugger.util debugger.cli
diff --git a/library/debugger/util.lean b/library/debugger/util.lean
new file mode 100644
index 0000000000..994d5ffb53
--- /dev/null
+++ b/library/debugger/util.lean
@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+namespace debugger
+def is_space (c : char) : bool :=
+if c = ' ' ∨ c = char.of_nat 11 ∨ c = '\n' then tt else ff
+
+def split_core : string → string → list string
+| (c::cs) [] :=
+  if is_space c then split_core cs [] else split_core cs [c]
+| (c::cs) r  :=
+  if is_space c then r^.reverse :: split_core cs [] else split_core cs (c::r)
+| []      [] := []
+| []      r  := [r^.reverse]
+
+def split (s : string) : list string :=
+(split_core s [])^.reverse
+
+def to_qualified_name_core : string → string → name
+| []      r := if r = [] then name.anonymous else mk_simple_name r^.reverse
+| (c::cs) r :=
+  if is_space c then to_qualified_name_core cs r
+  else if c = '.' then
+       if r = [] then to_qualified_name_core cs []
+       else           name.mk_string r^.reverse (to_qualified_name_core cs [])
+  else to_qualified_name_core cs (c::r)
+
+def to_qualified_name (s : string) : name :=
+to_qualified_name_core s []
+
+def olean_to_lean (s : string) :=
+list.dropn 5 s ++ "lean"
+
+meta def get_file (fn : name) : vm string :=
+do {
+  d ← vm.get_decl fn,
+  some n ← return (vm_decl.olean d) | failure,
+  return (olean_to_lean n)
+}
+<|>
+return "[current file]"
+
+meta def pos_info (fn : name) : vm string :=
+do {
+  d                ← vm.get_decl fn,
+  some (line, col) ← return (vm_decl.pos d) | failure,
+  file             ← get_file fn,
+  return (file ++ ":" ++ line^.to_string ++ ":" ++ col^.to_string)
+}
+<|>
+return "<position not available>"
+
+meta def show_fn (header : string) (fn : name) (frame : nat) : vm unit :=
+do pos ← pos_info fn,
+   vm.put_str ("[" ++ frame^.to_string ++ "] " ++ header),
+   if header = "" then return () else vm.put_str " ",
+   vm.put_str (fn^.to_string ++ " at " ++ pos ++ "\n")
+
+meta def show_curr_fn (header : string) : vm unit :=
+do fn ← vm.curr_fn,
+   sz ← vm.call_stack_size,
+   show_fn header fn (sz-1)
+
+meta def is_valid_fn_prefix (p : name) : vm bool :=
+do env ← vm.get_env,
+   return $ env^.fold ff (λ d r,
+     r ||
+     let n := d^.to_name in
+     p^.is_prefix_of n)
+
+meta def show_frame (frame_idx : nat) : vm unit :=
+do sz ← vm.call_stack_size,
+   fn ← if frame_idx >= sz then vm.curr_fn else vm.call_stack_fn frame_idx,
+   show_fn "" fn frame_idx
+
+meta def type_to_string : option expr → nat → vm string
+| none i := do
+  o ← vm.stack_obj i,
+  match o^.kind with
+  | vm_obj_kind.simple       := return "[tagged value]"
+  | vm_obj_kind.constructor  := return "[constructor]"
+  | vm_obj_kind.closure      := return "[closure]"
+  | vm_obj_kind.mpz          := return "[big num]"
+  | vm_obj_kind.name         := return "name"
+  | vm_obj_kind.level        := return "level"
+  | vm_obj_kind.expr         := return "expr"
+  | vm_obj_kind.declaration  := return "declaration"
+  | vm_obj_kind.environment  := return "environment"
+  | vm_obj_kind.tactic_state := return "tactic_state"
+  | vm_obj_kind.format       := return "format"
+  | vm_obj_kind.options      := return "options"
+  | vm_obj_kind.other        := return "[other]"
+  end
+| (some type) i := do
+  fmt ← vm.pp_expr type,
+  opts ← vm.get_options,
+  return (fmt^.to_string opts)
+
+meta def show_vars_core : nat → nat → nat → vm unit
+| c i e :=
+  if i = e then return ()
+  else do
+    (n, type) ← vm.stack_obj_info i,
+    type_str  ← type_to_string type i,
+    vm.put_str $ "#" ++ c^.to_string ++ " " ++ n^.to_string ++ " : " ++ type_str ++ "\n",
+    show_vars_core (c+1) (i+1) e
+
+meta def show_vars (frame : nat) : vm unit :=
+do (s, e) ← vm.call_stack_var_range frame,
+   show_vars_core 0 s e
+
+meta def show_stack_core : nat → vm unit
+| 0     := return ()
+| (i+1) := do
+  fn ← vm.call_stack_fn i,
+  show_fn "" fn i,
+  show_stack_core i
+
+meta def show_stack : vm unit :=
+do sz ← vm.call_stack_size,
+   show_stack_core sz
+end debugger
diff --git a/library/init/default.lean b/library/init/default.lean
index 470c0b0889..90be46c188 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -11,5 +11,5 @@ import init.funext init.function init.subtype init.classical init.congr
 import init.monad init.option init.state init.fin init.list init.char init.string init.to_string
 import init.monad_combinators init.set
 import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe
-import init.wf init.nat_div init.meta init.instances
+import init.wf init.nat_div init.meta init.instances init.breakpoint
 import init.sigma_lex init.id_locked init.order init.algebra
diff --git a/tmp/debugger_example.lean b/tmp/debugger_example.lean
new file mode 100644
index 0000000000..12c5d17e4b
--- /dev/null
+++ b/tmp/debugger_example.lean
@@ -0,0 +1,11 @@
+import debugger
+
+set_option debugger true
+set_option debugger.autorun true
+
+open tactic
+
+local attribute [breakpoint] tactic.constructor
+
+example (p q : Prop) : p → q → p ∧ q :=
+by do intros, constructor, repeat assumption